diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz new file mode 100644 index 0000000000000000000000000000000000000000..5128a06d909b5212142a8b93ed1b8682bd2dc144 Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz new file mode 100644 index 0000000000000000000000000000000000000000..4305ebcd23f63fbee7f0078b7f653a5e18f36e3c Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz index 8e690f6dd6a2a7823f8d660cc1314e7eb65140c2..a206ffbe35b7aa42bd28c17e0d52460beeda5757 100644 Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz differ diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz new file mode 100644 index 0000000000000000000000000000000000000000..cedfe06f6aac0f8a60f3c3dfb677246af8d442bf Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz differ diff --git a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err index a003a310ddaac2945e140ceaaaa6d7e3db90d6b4..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 --- a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err +++ b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err @@ -1,2 +0,0 @@ -<errors> -</errors> diff --git a/narration/IntegrationTests/SituationTheory.omdoc b/narration/IntegrationTests/SituationTheory.omdoc index a0c67cd22db68986c003641b23a181471ac2bb72..f6ce7cc4ef996431f7c0d896082cce0ff57cab3e 100644 --- a/narration/IntegrationTests/SituationTheory.omdoc +++ b/narration/IntegrationTests/SituationTheory.omdoc @@ -1,2 +1,2 @@ <?xml version="1.0" encoding="UTF-8"?> -<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1087.44.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/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:221.6.27"/></metadata></mref></omdoc> \ No newline at end of file +<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1966.78.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/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:220.6.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1535.56.0:1549.56.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1661.64.0:1681.64.20"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/relational/IntegrationTests/SituationTheory.rel b/relational/IntegrationTests/SituationTheory.rel index de23b8804434407870e731c8ac6f63b84ca0b344..76d8127407b0963dc4b74adf8c8fd7c2a9179203 100644 --- a/relational/IntegrationTests/SituationTheory.rel +++ b/relational/IntegrationTests/SituationTheory.rel @@ -1,2 +1,4 @@ document http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc -Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory +Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace +Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll +Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.rel new file mode 100644 index 0000000000000000000000000000000000000000..ea9bb58df091b1907cf972d401b9abaa9f9519e1 --- /dev/null +++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.rel @@ -0,0 +1,14 @@ +theory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll?Problem +theory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem?a +constant http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem?a +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll?Solution +theory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Includes http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution?c +constant http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution?c +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Solution?c?definition http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem?a?type diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel new file mode 100644 index 0000000000000000000000000000000000000000..4f69a9c6fcc6d2a724dd5c8f9f5331bfda1664e8 --- /dev/null +++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.rel @@ -0,0 +1,128 @@ +theory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace?Root +theory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen +Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Ded?DED?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Ded?DED?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?A?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?B?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Ded?DED?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace/Root?C?type diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel index c90b58ee35f5188837199e705ddf2a13f4013a4d..3fb3ea7acf55ba8b8f05b33eae8801ba8b36801a 100644 --- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel +++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel @@ -6,6 +6,8 @@ dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSi dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC theory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld?OppositeLen +Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld?AngleSum Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel new file mode 100644 index 0000000000000000000000000000000000000000..8b3bcb8c4742cb1f405622d6a1cd2219bb6fe45a --- /dev/null +++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.rel @@ -0,0 +1,23 @@ +theory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace?RootSituationTheory +theory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?v +HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem +HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory +view http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v +HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v?[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem]/a +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v?[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem]/a +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory/v?[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll/Problem]/a?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b?type +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace?PushedOutSituationTheory +theory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory +HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld?FrameworldMeta +Includes http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory +Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?c +constant http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?c +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/PushedOutSituationTheory?c?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace/RootSituationTheory?b?type diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt index c8898d35c209bdf9217165480aab0278d2fe8c51..8633382500516bea135bc43f67423ec8145e1185 100644 --- a/source/IntegrationTests/SituationTheory.mmt +++ b/source/IntegrationTests/SituationTheory.mmt @@ -4,42 +4,76 @@ import frameworld http://mathhub.info/FrameIT/frameworld âš fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš -theory SampleSituationTheory = - // planar triangle in R^2 â™ - - A - : point ☠- = ⟨0.0, 0.0, 0.0⟩ ☠- meta frameworld:?MetaAnnotations?label "A" - â™ - - B - : point ☠- = ⟨3.0, 3.0, 0.0⟩ ☠- meta frameworld:?MetaAnnotations?label "B" - â™ - - C - : point ☠- = ⟨0.0, 3.0, 0.0⟩ ☠- meta frameworld:?MetaAnnotations?label "C" - â™ - - distanceBC - : Σ x:â„. ⊦ (d- B C ≠x) ☠- = ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ☠- meta frameworld:?MetaAnnotations?label "BC" - â™ - - angleABC - : Σ β:â„. ⊦ ( ∠A,B,C ) ≠β ☠- = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ☠- meta frameworld:?MetaAnnotations?label "∠ABC" - â™ - - angleBAC - : Σ β:â„. ⊦ ( ∠A,B,C ) ≠β ☠- = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ☠- meta frameworld:?MetaAnnotations?label "∠BAC" - â™ +theory SampleSituationSpace = + theory Root = + // planar triangle in R^2 â™ + include ☞frameworld:?OppositeLen â™ + include ☞frameworld:?AngleSum â™ + + A + : point ☠+ = ⟨0.0, 0.0, 0.0⟩ ☠+ meta frameworld:?MetaAnnotations?label "ð”¸" + â™ + + B + : point ☠+ = ⟨3.0, 3.0, 0.0⟩ ☠+ meta frameworld:?MetaAnnotations?label "ð”¹" + â™ + + C + : point ☠+ = ⟨0.0, 3.0, 0.0⟩ ☠+ meta frameworld:?MetaAnnotations?label "â„‚" + â™ + + distanceBC + : Σ x:â„. ⊦ (d- B C ≠x) ☠+ = ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ☠+ meta frameworld:?MetaAnnotations?label "ð”¹â„‚" + â™ + + angleABC + : Σ β:â„. ⊦ ( ∠A,B,C ) ≠β ☠+ = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ☠+ meta frameworld:?MetaAnnotations?label "∠ð”¸ð”¹â„‚" + â™ + + angleBAC + : Σ β:â„. ⊦ ( ∠B,A,C ) ≠β ☠+ = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ☠+ meta frameworld:?MetaAnnotations?label "∠ℬð”¸â„‚" + â™ + + rightAngledC + : ⊦ ( ∠B,C,A ) ≠90.0 ☠+ = sketch "calculated by ComFreek by hand, hopefully correct" ☠+ meta frameworld:?MetaAnnotations?label "∟ℂ" + â™ + âš +âš + +theory MyScroll = + theory Problem = a: type â™âš + theory Solution = + include ?MyScroll/Problem â™ + c: type ☠= aâ™ + âš âš + +theory SituationSpace = + theory RootSituationTheory = + include ?MyScroll â™ + b: type â™ + + view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory = + a = b â™ + âš + âš + + theory PushedOutSituationTheory = + include ?SituationSpace/RootSituationTheory â™ + c: type ☠= b â™ + âš +âš \ No newline at end of file