Merge branch 'devel' of https://gl.mathhub.info/FrameIT/frameworld into devel

source/MetaTheories.mmt

-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 ❙
+❚

source/Scrolls/README.md

@@ -33,6 +33,9 @@ theory Midpoint =
                  to have access to the facts formalized in the problem theory ❙
         include ?Midpoint/Problem ❙
 
+        // the next meta annotations (to the theory) actually make this theory into a scroll: 
+           We specify the Problem and Solution theories  ❙
+
         meta ?MetaAnnotations?label "MidPoint" ❙
         meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
         meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙
@@ -52,10 +55,10 @@ theory Midpoint =
 
         midpoint
             : point ❘
-            = ⟨0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x)⟩ ❘
+            = ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩ ❘
             meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" ❘
             meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
         ❙
     ❚
 ❚
-```
\ No newline at end of file
+```