diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Circle$Area$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Circle$Area$Scroll.omdoc.xz
index 005e7693c95d19ab7ca06fd17b329cec29f8ec01..c06e6420a7fa14660016d68c73b6b9e717ca110f 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Circle$Area$Scroll.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Circle$Area$Scroll.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Circle$Line$Angle$To$Angle$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Circle$Line$Angle$To$Angle$Scroll.omdoc.xz
index e60b8f820dac883ca8c50cdec0cf6a3a422ab5f6..c7b76d1b02736043f5dbb538fb9a5e7458cbc871 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Circle$Line$Angle$To$Angle$Scroll.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Circle$Line$Angle$To$Angle$Scroll.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Circle$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Circle$Scroll.omdoc.xz
index 9319a7b1f417e914050cb53c0212fabea861acfe..c20fd5723a9e2a5418a0a9bdfe38e623f23b0fc8 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Circle$Scroll.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Circle$Scroll.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Cylinder$Volume$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Cylinder$Volume$Scroll.omdoc.xz
index 9757da144fc4b5c1b0bfd6b441e6cc20c00e4b50..41847b9e5a4d8ecf35eb0b19a09cbc423d224460 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Cylinder$Volume$Scroll.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Cylinder$Volume$Scroll.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz
index c2d4d9b4e41f9876a6cceff9497bdb7716ae1357..137df4f8fddfc860f75492213b363cd44bf925af 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Circle.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Circle.omdoc.xz
index 79a2490592fb2c8c738282c6bd9443d6e7ad4214..5d6a747d7384e8201f44e36e3133f5ffa3a60706 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Circle.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Circle.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cone.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cone.omdoc.xz
index 997f9a79e44e14b3d8554c14f8547e5509523d9d..9d9e47be11d42a86744d9dcfed6f163c7d7ff568 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cone.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cone.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cylinder.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cylinder.omdoc.xz
index 89100946620cbebd9287a711e200cba96055d75b..6f56a766303d6b964d92e9fa5776f0d9cdf3f04b 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cylinder.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cylinder.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.omdoc.xz
index 50a4734630113e0ecc6febdd5c42559544924a96..db0ff576635f708740d2463a3867a08c31bc8b52 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Triangles.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Triangles.omdoc.xz
index 60b270fd2493cb8d908572e1c702649a072bcaa6..f3c432f4ce093db28f338290268eff1564e20604 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Triangles.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Triangles.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
index 12e176b50fc740f4cdf9bc7ff91b4f6c9c85e709..f7d6899937c15db4fec53a8d751cc2a691afcfb9 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Parallel$Lines.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Parallel$Lines.omdoc.xz
index 39213a7a6e3bee616968480bbf3e76da8552c186..5bf8d8aa29020320965e0c7b120b34e74e597bef 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Parallel$Lines.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Parallel$Lines.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Truncated$Cone$Volume$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Truncated$Cone$Volume$Scroll.omdoc.xz
index 3e9639f78bb46cb9e1ffac95e6187b2b5feda7d6..226658eb88cdc484de89f39e112bb5edfb916358 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Truncated$Cone$Volume$Scroll.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Truncated$Cone$Volume$Scroll.omdoc.xz differ
diff --git a/narration/DefaultSituationSpace.omdoc b/narration/DefaultSituationSpace.omdoc
index 35190da0c5914f37cf3df3b1fe71ebc770e69df5..85328858cffa76012721c8eef2c54730259572f1 100644
--- a/narration/DefaultSituationSpace.omdoc
+++ b/narration/DefaultSituationSpace.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#0.0.0:781.29.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace]" target="http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#117.4.0:144.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#0.0.0:700.26.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace]" target="http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#117.4.0:144.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc
index 8234de0070e2b5a3521267367dd5d66a8f7df0e9..26c6c921aed12232c5c035c20c022252f3d3c62b 100644
--- a/narration/MetaTheories.omdoc
+++ b/narration/MetaTheories.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:23461.452.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#125.5.0:253.5.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#255.6.0:276.6.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?test1]" target="http://mathhub.info/FrameIT/frameworld?test1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#684.24.0:695.24.11"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?test2]" target="http://mathhub.info/FrameIT/frameworld?test2"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#787.31.0:798.31.11"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?2DPoints]" target="http://mathhub.info/FrameIT/frameworld?2DPoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#887.42.0:901.42.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITBasics]" target="http://mathhub.info/FrameIT/frameworld?FrameITBasics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#1296.66.0:1315.66.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITRectangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITRectangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#4802.127.0:4825.127.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTriangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITTriangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#7899.177.0:7921.177.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCircle]" target="http://mathhub.info/FrameIT/frameworld?FrameITCircle"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#11233.221.0:11252.221.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCone]" target="http://mathhub.info/FrameIT/frameworld?FrameITCone"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#15479.300.0:15496.300.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCylinder]" target="http://mathhub.info/FrameIT/frameworld?FrameITCylinder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#18893.355.0:18914.355.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTheories]" target="http://mathhub.info/FrameIT/frameworld?FrameITTheories"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#19856.378.0:19877.378.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#22899.432.0:22994.432.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#22996.433.0:23016.433.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:18663.390.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#125.5.0:253.5.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#255.6.0:276.6.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?test1]" target="http://mathhub.info/FrameIT/frameworld?test1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#684.24.0:695.24.11"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?test2]" target="http://mathhub.info/FrameIT/frameworld?test2"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#787.31.0:798.31.11"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?2DPoints]" target="http://mathhub.info/FrameIT/frameworld?2DPoints"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#887.42.0:901.42.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITBasics]" target="http://mathhub.info/FrameIT/frameworld?FrameITBasics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#1296.66.0:1315.66.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITRectangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITRectangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#4802.127.0:4825.127.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTriangles]" target="http://mathhub.info/FrameIT/frameworld?FrameITTriangles"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#7899.177.0:7921.177.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCircle]" target="http://mathhub.info/FrameIT/frameworld?FrameITCircle"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#10799.217.0:10818.217.19"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCone]" target="http://mathhub.info/FrameIT/frameworld?FrameITCone"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#13899.272.0:13916.272.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITCylinder]" target="http://mathhub.info/FrameIT/frameworld?FrameITCylinder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#16602.324.0:16623.324.21"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?FrameITTheories]" target="http://mathhub.info/FrameIT/frameworld?FrameITTheories"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#17565.347.0:17586.347.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#18101.370.0:18196.370.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#18198.371.0:18218.371.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/CircleScroll.omdoc b/narration/Scrolls/CircleScroll.omdoc
index 381010a8cd16b582173977a2cfa01f316b7d5876..33fa85e447590c9fe05c415e1a7afcd04bc10311 100644
--- a/narration/Scrolls/CircleScroll.omdoc
+++ b/narration/Scrolls/CircleScroll.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#0.0.0:5958.224.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#80.5.0:85.8.0"/></metadata><scope></scope></opaque><mref name="[http://mathhub.info/FrameIT/frameworld?CircleScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#90.12.0:108.12.18"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?CircleAreaScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleAreaScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#3529.110.1:3551.110.23"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?test]" target="http://mathhub.info/FrameIT/frameworld?test"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#4672.142.1:4682.142.11"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?test2]" target="http://mathhub.info/FrameIT/frameworld?test2"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#5332.173.0:5343.173.11"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#0.0.0:3349.132.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#80.5.0:85.8.0"/></metadata><scope></scope></opaque><mref name="[http://mathhub.info/FrameIT/frameworld?CircleScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#90.12.0:108.12.18"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?CircleAreaScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleAreaScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.mmt#2185.79.1:2207.79.23"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/ConeVolumeScroll.omdoc b/narration/Scrolls/ConeVolumeScroll.omdoc
index 35de24331fb92c45cb277da896980956119a528e..ab73e27bc412017077a3e5f7f9b010bdd89d0003 100644
--- a/narration/Scrolls/ConeVolumeScroll.omdoc
+++ b/narration/Scrolls/ConeVolumeScroll.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#0.0.0:9055.257.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#80.5.0:157.8.0"/></metadata>// This scrolls calculates the Volume of a cone with a circle as base. â™</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?ConeProblem]" target="http://mathhub.info/FrameIT/frameworld?ConeProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#160.10.0:177.10.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?ConeVolumeScroll]" target="http://mathhub.info/FrameIT/frameworld?ConeVolumeScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#1647.55.0:1669.55.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TruncatedConeProblem]" target="http://mathhub.info/FrameIT/frameworld?TruncatedConeProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#2668.80.0:2694.80.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TruncatedConeVolumeScroll]" target="http://mathhub.info/FrameIT/frameworld?TruncatedConeVolumeScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#3253.101.1:3284.101.32"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?CylinderVolumeScroll]" target="http://mathhub.info/FrameIT/frameworld?CylinderVolumeScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#5145.138.0:5171.138.26"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#0.0.0:6206.192.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#80.5.0:157.8.0"/></metadata>// This scrolls calculates the Volume of a cone with a circle as base. â™</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?ConeProblem]" target="http://mathhub.info/FrameIT/frameworld?ConeProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#160.10.0:177.10.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?ConeVolumeScroll]" target="http://mathhub.info/FrameIT/frameworld?ConeVolumeScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#1647.55.0:1669.55.22"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TruncatedConeProblem]" target="http://mathhub.info/FrameIT/frameworld?TruncatedConeProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#2668.80.0:2694.80.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?TruncatedConeVolumeScroll]" target="http://mathhub.info/FrameIT/frameworld?TruncatedConeVolumeScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#3253.101.1:3284.101.32"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?CylinderVolumeScroll]" target="http://mathhub.info/FrameIT/frameworld?CylinderVolumeScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ConeVolumeScroll.mmt#4826.136.0:4852.136.26"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/CylinderScroll.omdoc b/narration/Scrolls/CylinderScroll.omdoc
index 7f10c7b4f36dfbf6611fc282452d0e679cccad69..03f319417d9b475b0051aefbce42ef78d9ec35c2 100644
--- a/narration/Scrolls/CylinderScroll.omdoc
+++ b/narration/Scrolls/CylinderScroll.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/CylinderScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CylinderScroll.mmt#0.0.0:3688.108.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/CylinderScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/CylinderScroll.mmt#0.0.0:83.8.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/ParallelLines.omdoc b/narration/Scrolls/ParallelLines.omdoc
index deaa7f0254c5d555051fdc9d3c313a83a449a194..296b488b2b70c5be5d1de107144ee0969f711e06 100644
--- a/narration/Scrolls/ParallelLines.omdoc
+++ b/narration/Scrolls/ParallelLines.omdoc
@@ -1,5 +1,5 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.mmt#0.0.0:3623.98.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.mmt#80.5.0:285.23.0"/></metadata>S
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.mmt#0.0.0:3623.99.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.mmt#80.5.0:286.24.0"/></metadata>S
/|
/ |
/ |
@@ -15,4 +15,4 @@ D ----- C
| |
A ------B
-The scroll encodes the InterceptTheorem .</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?ParallelLines]" target="http://mathhub.info/FrameIT/frameworld?ParallelLines"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.mmt#289.26.0:308.26.19"/></metadata></mref></omdoc>
\ No newline at end of file
+The scroll encodes the InterceptTheorem .</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?ParallelLines]" target="http://mathhub.info/FrameIT/frameworld?ParallelLines"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/ParallelLines.mmt#290.27.0:309.27.19"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/PlaneLineAngleScroll.omdoc b/narration/Scrolls/PlaneLineAngleScroll.omdoc
index 5d567d7cf138e9c0d039be7bc11f9041277e3bc1..791afb92f380f3e55f4b666dc1b8c03eb8706062 100644
--- a/narration/Scrolls/PlaneLineAngleScroll.omdoc
+++ b/narration/Scrolls/PlaneLineAngleScroll.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#0.0.0:3621.96.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#80.5.0:157.8.0"/></metadata>// This scrolls calculates the Volume of a cone with a circle as base. â™</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?CircleLineAngleScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleLineAngleScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#165.15.0:192.15.27"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?CircleLineAngleToAngleScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleLineAngleToAngleScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#1662.48.0:1696.48.34"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#0.0.0:3590.96.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#80.5.0:157.8.0"/></metadata>// This scrolls calculates the Volume of a cone with a circle as base. â™</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?CircleLineAngleScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleLineAngleScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#165.15.0:192.15.27"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?CircleLineAngleToAngleScroll]" target="http://mathhub.info/FrameIT/frameworld?CircleLineAngleToAngleScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/PlaneLineAngleScroll.mmt#1662.48.0:1696.48.34"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/Scrolls/CircleScroll.rel b/relational/Scrolls/CircleScroll.rel
index ebb888c23d9a46f5880151d133b8c63645021ea8..47c342eebffb34be87d214a2bc7ae4d50420ffbb 100644
--- a/relational/Scrolls/CircleScroll.rel
+++ b/relational/Scrolls/CircleScroll.rel
@@ -1,5 +1,3 @@
document http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.omdoc
Declares http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.omdoc http://mathhub.info/FrameIT/frameworld?CircleScroll
Declares http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.omdoc http://mathhub.info/FrameIT/frameworld?CircleAreaScroll
-Declares http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.omdoc http://mathhub.info/FrameIT/frameworld?test
-Declares http://mathhub.info/FrameIT/frameworld/Scrolls/CircleScroll.omdoc http://mathhub.info/FrameIT/frameworld?test2
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
index 0f9afbcd4310fe2a7105d8963e245f0bc89b95e5..cd03b204d0e4ea3f1b417f204641b4a4b6f5d052 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
@@ -3,13 +3,12 @@ HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://math
Declares http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace?Root
theory http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root
HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?SupplementaryAngles
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?Pythagoras
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?CylinderVolumeScroll
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?CircleLineAngleToAngleScroll
-Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?test
-Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?test2
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?Midpoint
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?CircleScroll
Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?SinOppositeLeg
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.rel
index 153448b0462463b248c971f57a9338f4f34750fd..65658e3312afe1797149676726802190acb020ec 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.rel
@@ -1,5 +1,4 @@
dataconstructor http://mathhub.info/FrameIT/frameworld?FrameITTheories?makeCircleOf3EdgePoints
-dataconstructor http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA
theory http://mathhub.info/FrameIT/frameworld?FrameITTheories
HasMeta http://mathhub.info/FrameIT/frameworld?FrameITTheories http://cds.omdoc.org/urtheories?LF
Includes http://mathhub.info/FrameIT/frameworld?FrameITTheories http://mathhub.info/MitM/core/geometry?3DGeometry
@@ -50,10 +49,3 @@ DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?makeCircleOf3Ed
DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?makeCircleOf3EdgePoints?definition http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint?type
DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?makeCircleOf3EdgePoints?definition http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint?type
DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?makeCircleOf3EdgePoints?definition http://mathhub.info/FrameIT/frameworld?FrameITCircle?circleType3D?type
-Declares http://mathhub.info/FrameIT/frameworld?FrameITTheories http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA
-constant http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA
-DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
-DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?FrameITTheories?TestBrokenA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index c0dea9cf915f6e21b5860ce1c2465a55b8eee69f..a80c26c7a9f5114246fc1297d969258d5a6b290a 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -4,16 +4,14 @@ fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
theory DefaultSituationSpace =
theory Root =
- // include ?SupplementaryAngles â™
+ include ?SupplementaryAngles â™
include ?OppositeLen â™
include ?AngleSum â™
- // include ?ParallelLines â™
- // include ?InterceptTheorem â™
+ // include ?ParallelLines â™
+ // include ?InterceptTheorem â™
include ?Pythagorasâ™
include ?CylinderVolumeScrollâ™
include ?CircleLineAngleToAngleScrollâ™
- include ?testâ™
- include ?test2â™
include ?Midpoint â™
include ?CircleScroll â™
@@ -22,7 +20,6 @@ theory DefaultSituationSpace =
include ?CircleAreaScroll â™
include ?ConeVolumeScroll â™
include ?TruncatedConeVolumeScroll â™
- // include ?EqualCircleAreaScroll â™
âš
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index bb7cfcf4c0b4ce3fc8aca894e8a4a89ace82caa7..71a1893f1549b41967800825720c210670084bd4 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -198,9 +198,6 @@ theory FrameITTriangles =
trianglePerpendicularBisectorCA3D : triangle ⟶ line ☠= [t] from ( 0.5 rdotp ( ( _C t ) p+p ( _A t ) ) ) to ( ( 0.5 rdotp ( ( _C t ) p+p ( _A t ) ) ) p+p ( ( Pnormal ( Pof2Δ t ) ) Vcross ( ( _A t ) p-p ( _C t ) ) ) ) ☠# bisecTriCA3D 1 â™
trianglePerpendicularBisectorIntersectAxiom : { t } ⊦ colL ( bisecTriAB3D t ) ( bisecTriBC3D t) ☠# perpBisIntersectAxiomABBC 1 â™
- // this cant be the way to calculate it. Because we will not get a point with colV... ff â™
- // triangle_mid_point : triangle ⟶ point ☠= [t] colLV ( bisec_tri_AB_3d t ) ( bisec_tri_BC_3d t) ( perp_bis_intersect_axiom_AB_BC t ) ☠# mid_triangle_3d 1 â™
-
cramerRuleIntersection : point ⟶ point ⟶ point ⟶ ℠☠= [c,u,v] ( (-1.0 â‹… ( c _x ) â‹… ( v _y ) ) + ( ( c _y ) â‹… ( v _x ) ) ) / ( epsi + ( (-1.0 â‹… ( u _x ) â‹… ( v _y ) ) + ( ( u _y ) â‹… ( v _x ) )) ) ☠# CramerRuleIntersection 1 2 3 â™
// This function shouldn't be necessary. But due to some weird bug, the server will crash without it. â™
@@ -213,7 +210,6 @@ theory FrameITTriangles =
triangleMidPoint : triangle ⟶ point ☠= [t] intersectTwoLinesActualPoint ( bisecTriAB3D t ) ( bisecTriBC3D t) ☠# midTriangle3D 1 â™
triangleMidPointWrapper : point ⟶ point ⟶ point ⟶ point ☠= [p1,p2,p3] midTriangle3D ( Δ A B C ) ☠# midTriangle3DWrap 1 2 3 â™
- // triangle_perpendicular_bisectors_intersection_3d : triangle ⟶ point ☠= [t] ( ( 0.5 rdotp ( ( _A t ) p+p ( _B t ) ) ) ) ☠# mid_tri_3d 1 â™
@@ -228,22 +224,9 @@ theory FrameITCircle =
circleType3D : type ☠# circle â™
xcircleType3D : type ☠# xcircle ☠= plane × point × â„ â™
-
-
-
-
-
xcircleMidPoint: xcircle ⟶ point ☠# xmid 1 ☠= [c] Ï€l (Ï€r c) â™
-
-
-
-
-
-
-
-
// circle constructor taking a plane ( the circle lies in ) a point (middle) and a real number (radius) â™
circle3D : plane ⟶ point ⟶ ℠⟶ circle ☠# mkCirc3D 1 2 3 â™
@@ -275,16 +258,6 @@ theory FrameITCircle =
equalityCircles: circle ⟶ circle ⟶ bool ☠# equalCirc 1 2 â™
unequalityCircles : circle ⟶ circle ⟶ bool ☠# unequalCirc 1 2 â™
- // this should be literally illegal to do, but there is no other way to implement it because there is a certain axiom that is literally handing out proofs for everything.
- It will even proof you that 1==2. Don't ever use this unless you are 100% certain what you are doing â™
-
- // assignAreaValueProof: {c1: circle, erg: â„ } ⊦ areaCirc c1 ≠erg ☠# convA 1 2 â™
- // proofEqualCircles : { c1: circle, c2: circle, erg: â„, proof1: ( ⊦ areaCirc c1 ≠erg) , proof2: ( ⊦ areaCirc c2 ≠erg ) } ⊦ equalCirc c1 c2 ☠# axEqualCirc 1 2 3 4 5 â™
- // doIt : {c1: circle, c2: circle, areaBase : ( Σ x:â„ . ⊦ areaCirc c1 ≠x ) , areaTop : ( Σ x:â„ . ⊦ areaCirc c2 ≠x ) } ⊦ equalCirc c1 c2 â˜
- = [c1,c2,areaTop,areaBase] axEqualCirc c1 c2 (Ï€l areaBase) (convA c1 (Ï€l areaBase) ) (convA c2 (Ï€l areaTop) ) ☠# doz 1 2 3 4 â™
-
-
- // proofEqualCircles : {c1: circle, c2: circle, proof: ⊦ ( areaCirc c1 ) ≠( areaCirc c2 ) } ⊦ equalCirc c1 c2 ☠# axEqualCirc 1 2 %I3 â™
helperXyZ : point ⟶ point ⟶ ℠☠= [a,b] | a -- b | ☠# helpxyz 1 2 â™
@@ -293,7 +266,6 @@ theory FrameITCircle =
pointsToCircleCheckerTest : { M : point, A : point, B : point, MAsum: â„, MBsum: â„, ABsum: â„ , p1 : ⊦ ( MAsum ≠0.0 ), p2 : ⊦ ( MBsum ≠0.0 ) , p3 : ⊦ ( ABsum ≠0.0 ) } circle ☠= [M,A,B,p4,p5,p6,p7,p8,p9] mkCirc3D ( pToPlane M A B ) M (d- M A) ☠# pointsToCChecktest 1 2 3 4 5 6 %I7 %I8 %I9 â™
pointsToCircleWrapper : point ⟶ point ⟶ point ⟶ circle ☠= [M,A,B] pointsToCChecktest M A B (helpxyz M A) ( helpxyz M B ) ( helpxyz A B ) ☠# pointsToC 1 2 3 â™
- // pointsToCircleWrapper : point ⟶ point ⟶ point ⟶ circle ☠= [M,A,B] pointsToCChecktest M A B 1.0 1.0 1.0 ☠# pointsToC 1 2 3 â™
âš
@@ -336,19 +308,16 @@ theory FrameITCone =
axiomTruncatedConeBase : {c1, c2,p1, p2} ⊦ tconeBase ( mkTcone c1 c2 p1 p2) ≠c1 ☠role Simplify â™
axiomTruncatedConeTop : {c1, c2,p1, p2} ⊦ tconeTop ( mkTcone c1 c2 p1 p2) ≠c2 ☠role Simplify â™
- // truncated_cone_height : tcone ⟶ ℠☠= [tc] d- ( mid ( tcone_base tc ) ) ( mid ( tcone_top tc ) ) ☠# tcone_height 1 â™
// swapped top and base should be fine thoâ™
truncatedConeHeight : tcone ⟶ ℠☠= [tc] distPlP ( circlePlane ( tconeBase tc ) ) ( mid ( tconeTop tc ) ) ☠# tconeHeight 1 â™
- // truncatedConeBaseArea : tcone ⟶ ℠☠= [tc] ( real_pow ( radius ( tconeBase tc ) ) 2.0 ) + ( ( radius ( tconeTop tc ) ) â‹… ( radius ( tconeBase tc ) ) ) + ( real_pow ( radius ( tconeTop tc ) ) 2.0 ) ☠# tconeBaseArea 1 â™
truncatedConeArea : tcone ⟶ ℠☠= [tc] ( areaCirc ( tconeBase tc ) ) + ( ( ( radius ( tconeTop tc ) ) â‹… ( radius ( tconeBase tc ) ) ) â‹… pi_num ) + ( areaCirc ( tconeTop tc ) ) ☠# tconeArea 1 â™
truncatedConeVolume : tcone ⟶ ℠☠= [tc] ( 1.0 / 3.0 ) â‹… (tconeHeight tc) â‹… ( tconeArea tc ) ☠# tconeVol 1 â™
- // truncatedConeVolume : tcone ⟶ ℠☠= [tc] ( ( ( 1.0 / 3.0 ) â‹… pi_num ) â‹… (tconeHeight tc) ) â‹… ( ( real_pow ( radius ( tconeBase tc ) ) 2.0 ) + ( ( radius ( tconeTop tc ) ) â‹… ( radius ( tconeBase tc ) ) ) + ( real_pow ( radius ( tconeTop tc ) ) 2.0 ) ) ☠# tconeVol 1 â™
âš
@@ -387,41 +356,10 @@ theory FrameITTheories =
- // randomCircle : circle ☠# circulus â™
- // intersection_two_lines_test : line ⟶ line ⟶ ℠☠= [l,h] ( cramer_rule_intersection ( ( from l ) p-p (from h) ) ( direction_l l ) ( direction_l h ) ) ☠# intersect_two_lines_actual_point_test 1 2 â™
- // wrap_intersection_test : line ⟶ line ⟶ point ☠= [l,h] ( ( cramer_rule_intersection ( ( from l ) p-p ( from h ) ) ( direction_l l ) ( direction_l h ) ) rdotp ( direction_l l ) ) ☠# intersect_two_lines_wrap 1 2 â™
- // wrap_intersection_test2 : line ⟶ line ⟶ ℠☠= [l,h] ( cramer_rule_intersection ( ( from l ) p-p ( from h ) ) ( direction_l l ) ( direction_l h ) ) ☠# intersect_two_lines_wrap2 1 2 â™
- // wrap_wrap : line ⟶ line ⟶ point ☠= [l,h] ( intersect_two_lines_wrap2 l h ) rdotp ( direction_l l ) ☠# wrap_wrap_losing_mind 1 2 â™
-
- // wrap_wrapv2 : point ⟶ line ⟶ line ⟶ point ☠= [A,l,h] ( ( do_the_root ( 0.5 ) ) rdotp ( direction_l l ) ) ☠# wrap_wrap_losing_mindv2 1 2 3 â™
- // fast_equal : ℠⟶ ℠⟶ bool ☠= [a,b] | a p-p b | â™
- // ☠= [A,B] lineDirection A ∥ lineDirection B â™
- // parallelo: line ⟶ line ⟶ bool ☠# paraLL 1 2 â™
- // para_axio : { a: line , b: line } ⊦ paraLL a b ☠# cheat 1 2 â™
-
-
-
- // defining circle over 2 points. One for the center one for the edgeâ™
- // circleOf : point ⟶ point ⟶ circle ☠# mid 1 edge 2 â™
- // midpoint : circle ⟶ point ☠# mid 1 prec 1 â™
- // edgepoint : circle ⟶ point ☠# edge 1 prec 1 â™
- // axiom_midpoint : {p1,p2} ⊦ mid (mid p1 edge p2) ≠p1 ☠role ForwardRule â™
- // axiom_edgepoint : {p1,p2} ⊦ edge (mid p1 edge p2) ≠p2 ☠role ForwardRule â™
-
- // radius_circle : circle ⟶ ℠☠= [c] d- ( mid c ) (edge c) ☠# radius_circle 1 â™
- // circum_circle : circle ⟶ ℠☠= [c] ((d- ( mid c ) (edge c)) + (d- ( mid c ) (edge c))) â‹… pi_num ☠# circ_circ 1 â™
-
- // partial circlce circumference. x should be used in % â™
- // partial_circum_circle : circle ⟶ ℠⟶ ℠☠= [c,x] ((d- ( mid c ) (edge c)) + (d- ( mid c ) (edge c))) â‹… pi_num â‹… x ☠# partial_circ_circ 1 â™
-
- // area_circle : circle ⟶ ℠☠= [c] ((d- ( mid c ) (edge c)) â‹… (d- ( mid c ) (edge c))) â‹… pi_num ☠# area_circ 1 â™
-
- // use_actual_scp : point ⟶ ℠☠= [a] ( < a , a > ) ☠# do_actual_scp 1 â™
makeCircleOf3EdgePoints : point ⟶ point ⟶ point ⟶ circle ☠= [p1,p2,p3 ] mkCirc3D ( Ppara p1 (p2 p-p p1) ( p3 p-p p1) ) ( midTriangle3D ( Δ p1 p2 p3 ) ) ( d- ( midTriangle3D ( Δ p1 p2 p3 ) ) p1 ) ☠# mkCirc3P3D 1 2 3 â™
- TestBrokenA : ℠☠= 1.0 + 1 ☠# TestBroken â™
âš
diff --git a/source/Scrolls/CircleScroll.mmt b/source/Scrolls/CircleScroll.mmt
index 92fa350657d0f56c3b78abd95684e2a25a57a99d..5b3c4203a07ae5d57610d911d29316b56df0f669 100644
--- a/source/Scrolls/CircleScroll.mmt
+++ b/source/Scrolls/CircleScroll.mmt
@@ -27,23 +27,6 @@ theory CircleScroll =
theory Solution =
include ?CircleScroll/Problem â™
- // TODO: in the calculation a proof of interception should be used. But so far isnt. â™
- // deduceM : point â˜
- = intersect_two_lines_actual_point ( bisec_tri_BC_3d ( Δ A B C ) ) ( bisec_tri_AB_3d ( Δ A B C ) ) â˜
- meta ?MetaAnnotations?label "M" â˜
- meta ?MetaAnnotations?description "Middle of the circle"
- â™
-
-
- // deduceR : Σ x:â„ . ⊦ ( d- deduceM A) ≠x â˜
- = ⟨ ( d- deduceM A) , sketch "deduce Radius"⟩ â˜
-
- meta ?MetaAnnotations?label "R" â˜
- meta ?MetaAnnotations?description "radius of C"
- â™
-
-
- // = mkCirc3D ( pToPlane M A B ) M (d- M A) â™
deduceC
: circle â˜
@@ -81,22 +64,8 @@ theory CircleScroll =
- // deduceE : plane â˜
-
- = Ppara A B C â˜
- meta ?MetaAnnotations?label s"PlaceHolder${lverb Azzz }" â˜
- meta ?MetaAnnotations?description s"Deduce a circle from 3 points on its edge "
- â™
-
- // deduceCircle a
- : Σ x:â„ . ⊦ ( circ_circ (mid M edge E) ) ≠x â˜
- = ⟨((Ï€l distanceME) + (Ï€l distanceME)) â‹… pi_num , sketch "CircleCircumference Scroll"⟩ â˜
- meta ?MetaAnnotations?label s"PlaceHolder${lverb M E}" â˜
- meta ?MetaAnnotations?description s"xThe deduced circumference of the circle "
- â™
-
// the description verbalizes CircleCircumference, hence must come after its declaration â™
meta ?MetaAnnotations?label "CircleScroll" â™
meta ?MetaAnnotations?description s"Calculating a circle defined by the middle ${lverb M}, an edge point ${lverb A} and a point on the circle plane ${lverb B}. " â™
@@ -140,67 +109,6 @@ theory CircleScroll =
- theory test =
- meta ?MetaAnnotations?problemTheory ?test/Problem â™
- meta ?MetaAnnotations?solutionTheory ?test/Solution â™
-
-
- theory Problem =
-
- K : point ☠meta ?MetaAnnotations?label "C" â™
-
-
-
- âš
-
- theory Solution =
- include ?test/Problem â™
-
-
-
- test : â„ â˜
- = TestBroken â˜
- meta ?MetaAnnotations?label s"BIG FAN" â˜
- meta ?MetaAnnotations?description s"length "
-
- â™
-
-
- meta ?MetaAnnotations?label "testscroll" â™
- meta ?MetaAnnotations?description s" Example Scroll for testing" â™
- âš
- âš
-
-theory test2 =
- meta ?MetaAnnotations?problemTheory ?test2/Problem â™
- meta ?MetaAnnotations?solutionTheory ?test2/Solution â™
-
-
- theory Problem =
-
- M : point ☠meta ?MetaAnnotations?label "M" â™
-
-
- âš
-
- theory Solution =
- include ?test2/Problem â™
-
-
-
- deduceThis : â„ â˜
- = 1.0 + 1.0 â˜
- meta ?MetaAnnotations?label s"r" â˜
- meta ?MetaAnnotations?description s"Radius "
- â™
-
-
- meta ?MetaAnnotations?label "testscroll2" â™
- meta ?MetaAnnotations?description s" calculates the radius of a given circle" â™
- âš
- âš
-
-
diff --git a/source/Scrolls/ConeVolumeScroll.mmt b/source/Scrolls/ConeVolumeScroll.mmt
index de50f2c211b661c78a36082454c9837cf24f24d2..a1f7684c51cd6cb34f2a77950104b19ae6ba8b98 100644
--- a/source/Scrolls/ConeVolumeScroll.mmt
+++ b/source/Scrolls/ConeVolumeScroll.mmt
@@ -116,8 +116,6 @@ theory TruncatedConeProblem =
theory Solution =
include ?TruncatedConeVolumeScroll/Problem â™
- // = ⟨ doDiv ( ( ( real_pow ( radius ( circle1 ) ) 2.0 ) + ( ( radius ( circle1 ) ) â‹… ( radius ( circle2 ) ) ) + ( real_pow ( radius ( circle2 ) ) 2.0 ) ) â‹… ( Ï€l height )â‹… pi_num ) 3.0 , sketch "TruncatedConeVolume Scroll" ⟩ â˜â™
-
deduceVolume
: Σ x : â„ . ⊦ ( tconeVol ( mkTcone base top proofOfUnEqualSize ( axParaCirc base top H orthoBaseH orthoTopH ) ) ) ≠x â˜
= ⟨ doDiv ( ( ( Ï€l areaBase ) + ( doRoot ( ( Ï€l areaBase ) â‹… ( Ï€l areaTop ) ) ) + ( Ï€l areaTop ) ) â‹… ( Ï€l height ) ) 3.0 , sketch "TruncatedConeVolume Scroll" ⟩ â˜
@@ -156,12 +154,7 @@ theory CylinderVolumeScroll =
theory Solution =
include ?CylinderVolumeScroll/Problem â™
- // deduceCylinder
- : cyl â˜
- = mkCyl circle1 circle2 ( axParaCirc circle1 circle2 heightLine orthHeiBase orthHeiTop ) â˜
- meta ?MetaAnnotations?label s"Z:${lverb circle1 circle2} " â˜
- meta ?MetaAnnotations?description s"Cylinder"
- â™
+
@@ -184,64 +177,6 @@ theory CylinderVolumeScroll =
-// theory EqualCircleAreaScroll =
- meta ?MetaAnnotations?problemTheory ?EqualCircleAreaScroll/Problem â™
- meta ?MetaAnnotations?solutionTheory ?EqualCircleAreaScroll/Solution â™
-
- theory Problem =
-
-
-
- circle1 : circle ☠meta ?MetaAnnotations?label "â—‹C" â™
- circle2 : circle ☠meta ?MetaAnnotations?label "â—‹c" â™
-
-
- areaBase : Σ x:â„ . ⊦ areaCirc circle1 ≠x â˜
- meta ?MetaAnnotations?label s"A1" â˜
- meta ?MetaAnnotations?description s"Area of base ${lverb circle1}"
-
- â™
- areaTop : Σ x:â„ . ⊦ areaCirc circle2 ≠x â˜
- meta ?MetaAnnotations?label s"A2" â˜
- meta ?MetaAnnotations?description s"Area of base ${lverb circle2}"
-
- â™
-
-
-
- âš
-
-// theory Solution =
- include ?EqualCircleAreaScroll/Problem â™
- // deduceCylinder
- : cyl â˜
- = mkCyl circle1 circle2 ( axParaCirc circle1 circle2 heightLine orthHeiBase orthHeiTop ) â˜
- meta ?MetaAnnotations?label s"Z:${lverb circle1 circle2} " â˜
- meta ?MetaAnnotations?description s"Cylinder"
- â™
-
-// = axEqualCirc circle1 circle2 (Ï€l areaBase) (convA circle1 (Ï€l areaBase) ) (convA circle2 (Ï€l areaTop) ) â˜
-
- = axEqualCirc circle1 circle2 (Ï€l areaBase) (convA circle1 (Ï€l areaBase) ) (convA circle2 (Ï€l areaTop) ) ☠â™
-
-
- equalCircleFact
- : ⊦ equalCirc circle1 circle2 â˜
- // = axEqualCirc circle1 circle2 (Ï€l areaBase) (convA circle1 (Ï€l areaBase) ) (convA circle2 (Ï€l areaTop) ) â˜
- meta ?MetaAnnotations?label s"${lverb circle1}=${lverb circle2} " â˜
- meta ?MetaAnnotations?description s"EqualAreaCircles"
- â™
-
- meta ?MetaAnnotations?label "EqualCircleAreaScroll" â™
- meta ?MetaAnnotations?description s"This scroll checks whether the area of the 2 given circles ${lverb circle1} ${lverb circle1} is equal or not." â™
-
- âš
-// âš
-
-
-
-
-
diff --git a/source/Scrolls/CylinderScroll.mmt b/source/Scrolls/CylinderScroll.mmt
index 18e498252c7c80898710ac5c68d580fd7cf29f45..5e214e94cf852f7b997e9a6d981a1c15352fa320 100644
--- a/source/Scrolls/CylinderScroll.mmt
+++ b/source/Scrolls/CylinderScroll.mmt
@@ -2,106 +2,6 @@ namespace http://mathhub.info/FrameIT/frameworld âš
fixmeta ?FrameworldMeta âš
-// theory CylinderVolumeScroll =
- meta ?MetaAnnotations?problemTheory ?CylinderVolumeScroll/Problem â™
- meta ?MetaAnnotations?solutionTheory ?CylinderVolumeScroll/Solution â™
-
- theory Problem =
- include ?ConeVolumeScroll/Problem â™
-
-
- proofOfEqualSize : ⊦ equalCirc base top â˜
- meta ?MetaAnnotations?label s"${lverb base}=${lverb top}" â˜
- meta ?MetaAnnotations?description s"Proof of equally sized Areas"
-
- â™
-
-
-
- âš
-
- // theory Solution =
- include ?CylinderVolumeScroll/Problem â™
- // deduceCylinder
- : cyl â˜
- = mkCyl circle1 circle2 ( axParaCirc circle1 circle2 heightLine orthHeiBase orthHeiTop ) â˜
- meta ?MetaAnnotations?label s"Z:${lverb circle1 circle2} " â˜
- meta ?MetaAnnotations?description s"Cylinder"
- â™
-
-
-
- deduceVolume
- : Σ x : â„ . ⊦ ( cylVol ( mkCyl circle1 circle2 proofOfEqualSize ( axParaCirc circle1 circle2 heightLine orthHeiBase orthHeiTop ) ) ) ≠x â˜
- = ⟨ ( Ï€l height ) â‹… ( Ï€l area_base ) , sketch "CylinderVolume Scroll" ⟩ â˜
- meta ?MetaAnnotations?label s"V:${lverb circle1 circle2} " â˜
- meta ?MetaAnnotations?description s"The Volume of the Cylinder"
- â™
-
- meta ?MetaAnnotations?label "CylinderVolumeScroll" â™
- meta ?MetaAnnotations?description s"This scroll caclculates the volume of a cylinder with top ${lverb circle2}, base ${lverb circle1}, height ${lverb height} and intersection points ${lverb I1} and ${lverb I2}. The formula is V = ${lverb height} â‹… ${lverb area_base} . " â™
-
- âš
-// âš
-
-
-
-
-
-
-
-// theory EqualCircleAreaScroll =
- meta ?MetaAnnotations?problemTheory ?EqualCircleAreaScroll/Problem â™
- meta ?MetaAnnotations?solutionTheory ?EqualCircleAreaScroll/Solution â™
-
- // theory Problem =
-
-
-
- circle1 : circle ☠meta ?MetaAnnotations?label "â—‹C" â™
- circle2 : circle ☠meta ?MetaAnnotations?label "â—‹c" â™
-
-
- areaBase : Σ x:â„ . ⊦ areaCirc circle1 ≠x â˜
- meta ?MetaAnnotations?label s"A1" â˜
- meta ?MetaAnnotations?description s"Area of base ${lverb circle1}"
-
- â™
- areaTop : Σ x:â„ . ⊦ areaCirc circle2 ≠x â˜
- meta ?MetaAnnotations?label s"A2" â˜
- meta ?MetaAnnotations?description s"Area of base ${lverb circle2}"
-
- â™
-
-
-
- âš
-
- // theory Solution =
- include ?EqualCircleAreaScroll/Problem â™
- // deduceCylinder
- : cyl â˜
- = mkCyl circle1 circle2 ( axParaCirc circle1 circle2 heightLine orthHeiBase orthHeiTop ) â˜
- meta ?MetaAnnotations?label s"Z:${lverb circle1 circle2} " â˜
- meta ?MetaAnnotations?description s"Cylinder"
- â™
-
-
-
- equalCircleFact
- : ⊦ equalCirc circle1 circle2 â˜
- = axEqualCirc circle1 circle2 â˜
- meta ?MetaAnnotations?label s"${lverb circle1}=${lverb circle1} " â˜
- meta ?MetaAnnotations?description s"EqualAreaCircles"
- â™
-
- meta ?MetaAnnotations?label "EqualCircleAreaScroll" â™
- meta ?MetaAnnotations?description s"This scroll checks whether the area of the 2 given circles ${lverb circle1} ${lverb circle1} is equal or not." â™
-
- âš
-// âš
-
-
diff --git a/source/Scrolls/ParallelLines.mmt b/source/Scrolls/ParallelLines.mmt
index 8b6276a8a2606448304e6edbd2c988cf72b164ce..e52d466b494829df3af288a58ddd8821d34035cb 100644
--- a/source/Scrolls/ParallelLines.mmt
+++ b/source/Scrolls/ParallelLines.mmt
@@ -21,6 +21,7 @@ D ----- C
A ------B
The scroll encodes the InterceptTheorem .
+
âš
@@ -93,6 +94,6 @@ theory ParallelLines =
// the description verbalizes ParallelLines, hence must come after its declaration â™
// This Scrolls deduces whether the two lines ${lverb AB} and ${lverb CD} are parallel or not. â™
meta ?MetaAnnotations?label s"ParallelLines" â™
- meta ?MetaAnnotations?description "sThe opposing sides of a rectangular ABCD are always parallel" â™
+ meta ?MetaAnnotations?description " The opposing sides of a rectangular ABCD are always parallel" â™
âš
âš
diff --git a/source/Scrolls/PlaneLineAngleScroll.mmt b/source/Scrolls/PlaneLineAngleScroll.mmt
index 5937f0cacb7fbb320fbdf4c703017a611c3063de..81f9989255c57e1045850e2c80847f1c4afa40ae 100644
--- a/source/Scrolls/PlaneLineAngleScroll.mmt
+++ b/source/Scrolls/PlaneLineAngleScroll.mmt
@@ -82,7 +82,7 @@ theory CircleLineAngleToAngleScroll =
theory Solution =
include ?CircleLineAngleToAngleScroll/Problem â™
- // radToDegree ( ∠P,B,A ) â™
+
deduceAngle : Σ x : â„ . ⊦ ( ∠P,B,A ) ≠x â˜
= ⟨ Ï€l planeLineAngle , sketch "CastAngle" ⟩ â˜
meta ?MetaAnnotations?label s"∠${lverb P B A}" â˜