Skip to content
Snippets Groups Projects
Commit d015e5f7 authored by ki7077's avatar ki7077
Browse files

Deleted old code 

clean up
parent 9ffaac60
Branches marcel
No related tags found
1 merge request!1Added new Scrolls and new Theories
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 42 deletions
content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Basics.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Circle.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cone.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Cylinder.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Rectangles.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Theories.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/$Frame$I$T$Triangles.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
content/http..mathhub.info/FrameIT/frameworld/2$D$Points.omdoc.xz
+ 0
− 0
View file @ d015e5f7
No preview for this file type
narration/MetaTheories.omdoc
+ 1
− 1
View file @ d015e5f7
<?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
relational/MetaTheories.rel
+ 0
− 2
View file @ d015e5f7
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
......
source/MetaTheories.mmt
+ 0
− 39
View file @ d015e5f7
......@@ -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 ❙
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment