Added SupplementaryAngles-Scroll to DefaultSituationSpace

errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err

+<errors>
+</errors>

narration/DefaultSituationSpace.omdoc

 <?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:259.10.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:300.12.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

narration/IntegrationTests/SituationTheory.omdoc

 <?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:1753.61.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/space_typechecking_test"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><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/space_typechecking_test?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#271.7.0:291.7.20"/></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:2475.84.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/space_typechecking_test"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><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/space_typechecking_test?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#271.7.0:291.7.20"/></metadata></mref></omdoc>
\ No newline at end of file

narration/Library/gearbox.omdoc

 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2736.75.68"/><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/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2739.77.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/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref></omdoc>
\ No newline at end of file

narration/MetaTheories.omdoc

 <?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:1072.33.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#70.4.0:198.4.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#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#628.22.0:723.22.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#725.23.0:745.23.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:1074.34.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#70.4.0:198.4.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#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#628.22.0:723.22.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#725.23.0:745.23.20"/></metadata></mref></omdoc>
\ No newline at end of file

narration/Scrolls/SupplementaryAngles.omdoc

 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#0.0.0:1612.46.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/SupplementaryAngles.mmt#78.3.0:245.11.0"/></metadata><scope>\
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#0.0.0:1623.46.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/SupplementaryAngles.mmt#78.3.0:245.11.0"/></metadata><scope>\
        \ D
         \
  ________\_________

relational/Scrolls/.rel

@@ -2,3 +2,4 @@ document http://mathhub.info/FrameIT/frameworld/Scrolls
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/gearbox.omdoc

relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel

@@ -3,6 +3,7 @@ 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?Midpoint

source/DefaultSituationSpace.mmt

@@ -4,6 +4,7 @@ fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
 
 theory DefaultSituationSpace =
     theory Root =
+        include ?SupplementaryAngles ❙
         include ?OppositeLen ❙
         include ?AngleSum ❙
         include ?Midpoint ❙

source/Scrolls/SupplementaryAngles.mmt

@@ -32,7 +32,7 @@ theory SupplementaryAngles =
     ❚
 
     theory Solution =
-        meta ?MetaAnnotations?label "AngleSum" ❙
+        meta ?MetaAnnotations?label "SupplementaryAngles" ❙
         meta ?MetaAnnotations?description "Supplementary angles add up to 180 degree " ❙
 
         include ?SupplementaryAngles/Problem ❙