diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index d4537efa5248828c8aa8f708e8da778e729280c7..5d74cd0ad7a3adfd65cfab41f1a571040256f4dc 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -1,34 +1,34 @@ -namespace http://mathhub.info/FrameIT/frameworld âš - -fixmeta ur:?LF âš - -/T MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls âš -theory MetaAnnotations = - include ☞http://mathhub.info/MitM/Foundation?Strings â™ - - label â™ - description â™ - - problemTheory â™ - solutionTheoryâ™ - - /T Example usages: - - `lverb A`, where A refers to a symbol - - `lverb A B`, a shorthand for `concat (lverb A) (lverb B)`; works for arbitrary number of arguments - â™ - label_verbalization_of # lverb â™ - description_verbalization_of # dverb â™ -âš - -/T The meta theory to use for situation theories, scroll problem, and scroll solution theories âš -theory FrameworldMeta = - include ?MetaAnnotations â™ - - include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma â™ - - include ☞http://mathhub.info/MitM/Foundation?Strings â™ - include ☞http://mathhub.info/MitM/Foundation?Math â™ - - include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™ - include ☞http://mathhub.info/MitM/core/geometry?Planes â™ -âš +namespace http://mathhub.info/FrameIT/frameworld âš + +fixmeta ur:?LF âš + +/T MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls âš +theory MetaAnnotations = + include ☞http://mathhub.info/MitM/Foundation?Strings â™ + + label â™ + description â™ + + problemTheory â™ + solutionTheoryâ™ + + /T Example usages: + - `lverb A`, where A refers to a symbol + - `lverb A B`, a shorthand for `concat (lverb A) (lverb B)`; works for arbitrary number of arguments + â™ + label_verbalization_of # lverb â™ + description_verbalization_of # dverb â™ +âš + +/T The meta theory to use for situation theories, scroll problem, and scroll solution theories âš +theory FrameworldMeta = + include ?MetaAnnotations â™ + + include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma â™ + + include ☞http://mathhub.info/MitM/Foundation?Strings â™ + include ☞http://mathhub.info/MitM/Foundation?Math â™ + + include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™ + include ☞http://mathhub.info/MitM/core/geometry?Planes â™ +âš