diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Basics.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Basics.omdoc.xz index ee7a231f64e1880394cf309bdb346cd00545618a..2dfcbf1bae7dd7fecb0db46054d4f257f67b16b4 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Basics.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Basics.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 5d6a747d7384e8201f44e36e3133f5ffa3a60706..c550d517c998eebcb934a89888a11845324999fe 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 9d9e47be11d42a86744d9dcfed6f163c7d7ff568..25b921cc470e49855198ea5e309e6b2c604a2e71 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 6f56a766303d6b964d92e9fa5776f0d9cdf3f04b..7ab3750993012ac5c4078bc00d51ef5d7842f3ef 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$Rectangles.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Rectangles.omdoc.xz index a7c0bb7c3605108a466417ac95116a6778f62946..fe144b5eeb839f794768ed8df3f44e96dd4a8170 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Rectangles.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Rectangles.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 db0ff576635f708740d2463a3867a08c31bc8b52..ef4bdc99ff6e8c85c5bd29610871e7ee0a583d7f 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 f3c432f4ce093db28f338290268eff1564e20604..89177af6ff6b8faef7d74a953730f17bb1220894 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 f7d6899937c15db4fec53a8d751cc2a691afcfb9..77d6bc0db3eba5dbade242d1f7e76b4d337f747a 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/2$D$Points.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/2$D$Points.omdoc.xz index 21befeea26c38aa6afbf9e9631382df77891de46..e344ec3aab6690ac42568d1f150ab962c954ed89 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/2$D$Points.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/2$D$Points.omdoc.xz differ diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc index 26c6c921aed12232c5c035c20c022252f3d3c62b..d21abeaf01c1cf421abf3708891523874bee15f8 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: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 +<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:18180.351.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?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#684.24.0:698.24.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#1085.40.0:1104.40.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#4498.100.0:4521.100.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#7595.150.0:7617.150.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#10326.188.0:10345.188.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#13426.243.0:13443.243.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#16129.295.0:16150.295.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#17092.318.0:17113.318.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#17618.331.0:17713.331.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#17715.332.0:17735.332.20"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/relational/MetaTheories.rel b/relational/MetaTheories.rel index 352653f595342331291480db90173b6eb4981f60..6b8fa1982acbe47a182d7f0fba9ba416ab6d3a05 100644 --- a/relational/MetaTheories.rel +++ b/relational/MetaTheories.rel @@ -1,7 +1,5 @@ document http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?MetaAnnotations -Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?test1 -Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?test2 Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?2DPoints Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITBasics Declares http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc http://mathhub.info/FrameIT/frameworld?FrameITRectangles diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 71a1893f1549b41967800825720c210670084bd4..1e7a1d1f4a967b9caa8fbd2fdc9eaeb1c198dcd6 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -22,24 +22,6 @@ theory MetaAnnotations = âš -theory test1 : ur:?LF = - include ?FrameITBasics â™ - - xA : point ☠= ⟨0.5, 0.5, 0.5⟩ â™ - -âš - -theory test2 : ur:?LF = - include ?test1 â™ - - xA : point ☠= ⟨5.5, 5.5, 5.5⟩ â™ - - - -âš - - - theory 2DPoints = include ?FrameITBasics â™ @@ -54,16 +36,8 @@ theory 2DPoints = YPoint2D : point2d ⟶ ℠☠# p2y 1 â™ YPoint2DAxiom : {x,y} ⊦ ( p2y (mkpoint2d x y ) ) ≠y ☠role Simplify â™ - - - - - âš - - - theory FrameITBasics = include ☞http://mathhub.info/MitM/core/geometry?3DGeometry â™ include ☞http://mathhub.info/MitM/core/geometry?Planes â™ @@ -71,7 +45,6 @@ theory FrameITBasics = // Basics for FrameIT theories â™ // a lot of Simplify roles, so the scrolls get simplified accordingly â™ - // com_dist : {p1: point,p2: point} ⊦ ( d- p1 p2 ) ≠( d- p2 p1 ) ☠role Simplify â™ axiomrealNumbersNeutralLeft : {x: â„ } ⊦ 1.0 â‹… x ≠x ☠role Simplify â™ axiomrealNumbersNeutralRight : {x: â„ } ⊦ x â‹… 1.0 ≠x ☠role Simplify â™ @@ -203,10 +176,8 @@ theory FrameITTriangles = // This function shouldn't be necessary. But due to some weird bug, the server will crash without it. â™ wrapCramerRuleIntersectionForIntersectingBisectors : line ⟶ line ⟶ ℠☠= [l,h] ( cramerRuleIntersection ( ( from l ) p-p ( from h ) ) ( directionL l ) ( directionL h ) ) ☠# CramerRuleIntersectionLines 1 2 â™ - // wrap_cramer_rule_intersection_for_intersecting_bisectors : {l: line,h: line} ( ⊦ colL l h ) â™ intersectionTwoLines : line ⟶ line ⟶ point ☠= [l,h] ( from l ) p+p ( ( CramerRuleIntersectionLines l h ) rdotp ( directionL l ) ) ☠# intersectTwoLinesActualPoint 1 2 â™ - // ( perp_bis_intersect_axiom_AB_BC t )â™ 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 â™ @@ -354,20 +325,10 @@ theory FrameITTheories = include ?FrameITCone â™ include ?FrameITCylinder â™ - - - - 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 â™ - - âš - - - - /T The meta theory to use for situation theories, scroll problem, and scroll solution theories âš theory FrameworldMeta = include ?MetaAnnotations â™