feat: label interpolation in the going

54d9b2b0 · ComFreek · 1be1f9b9 · 54d9b2b0 · 54d9b2b0 · 54d9b2b0
Commit 54d9b2b0 authored 4 years ago by ComFreek
--- a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz
--- a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz
+++ b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz
--- 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
--- a/errors/mmt-omdoc/MetaTheories.mmt.err
+++ b/errors/mmt-omdoc/MetaTheories.mmt.err
-<errors>
-</errors>
--- a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
+++ b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
--- a/narration/IntegrationTests/SituationTheory.omdoc
+++ b/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:1233.42.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="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#134.4.0:161.4.27"/></metadata></mref></omdoc>
+<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
--- a/narration/MetaTheories.omdoc
+++ b/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:804.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://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#358.14.0:453.14.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#455.15.0:475.15.20"/></metadata></mref></omdoc>
+<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:888.30.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#442.18.0:537.18.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#539.19.0:559.19.20"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/narration/Scrolls/TriangleScrolls.omdoc
+++ b/narration/Scrolls/TriangleScrolls.omdoc
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4188.123.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/TriangleScrolls.mmt#79.4.0:273.13.0"/></metadata>A blueprint problem theory for triangle scrolls
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4731.124.3"/><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/TriangleScrolls.mmt#79.4.0:273.13.0"/></metadata>A blueprint problem theory for triangle scrolls
       B
      /|
     / |
@@ -7,6 +7,6 @@
   /___|
  A    C
-  (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#275.14.0:310.14.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#479.20.0:635.22.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle
+  (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#275.14.0:310.14.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#579.20.0:735.22.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle
-   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#637.23.0:676.23.39"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#846.31.0:860.31.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1946.62.0:1963.62.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?Pythagoras]" target="http://mathhub.info/FrameIT/frameworld?Pythagoras"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#3037.93.0:3053.93.16"/></metadata></mref></omdoc>
+   We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#737.23.0:776.23.39"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#946.31.0:960.31.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2046.62.0:2063.62.17"/></metadata></mref></omdoc>
\ No newline at end of file
--- a/relational/Scrolls/TriangleScrolls.rel
+++ b/relational/Scrolls/TriangleScrolls.rel
@@ -3,4 +3,3 @@ Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc ht
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?AngleSum
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?OppositeLen
-Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?Pythagoras
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
@@ -60,4 +60,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angl
 DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
 DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
@@ -2,6 +2,7 @@ untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label
 untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?description
 untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?problemTheory
 untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory
+untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of
 theory http://mathhub.info/FrameIT/frameworld?MetaAnnotations
 HasMeta http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://cds.omdoc.org/urtheories?LF
 Includes http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/MitM/Foundation?Strings
@@ -13,3 +14,5 @@ Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.i
 constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?problemTheory
 Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory
 constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory
+Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of
+constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
@@ -58,4 +58,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solutio
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel
@@ -41,3 +41,28 @@ DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?
 DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
 DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?trivial?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Strings?string?type
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel
@@ -47,7 +47,7 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?C?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
@@ -73,7 +73,7 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?B?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
@@ -99,4 +99,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?B?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -10,36 +10,36 @@ theory SampleSituationTheory =
    A
        : point ❘
        = ⟨0.0, 0.0, 0.0⟩ ❘
-        meta frameworld:?MetaAnnotations?label "Point A"
+        meta frameworld:?MetaAnnotations?label "A"
   ❙
    B
        : point ❘
        = ⟨3.0, 3.0, 0.0⟩ ❘
-        meta frameworld:?MetaAnnotations?label "Point B"
+        meta frameworld:?MetaAnnotations?label "B"
   ❙
    C
        : point ❘
        = ⟨0.0, 3.0, 0.0⟩ ❘
-        meta frameworld:?MetaAnnotations?label "Point C"
+        meta frameworld:?MetaAnnotations?label "C"
   ❙
   distanceBC
        : Σ x:ℝ. ⊦ (d- B C ≐ x) ❘
        = ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ❘
-        meta frameworld:?MetaAnnotations?label "distanceBC"
+        meta frameworld:?MetaAnnotations?label "BC"
   ❙
   angleABC
        : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
        = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
-        meta frameworld:?MetaAnnotations?label "distanceBC"
+        meta frameworld:?MetaAnnotations?label "∠ABC"
   ❙
   angleBAC
        : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
        = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
-        meta frameworld:?MetaAnnotations?label "distanceBC"
+        meta frameworld:?MetaAnnotations?label "∠BAC"
   ❙
 ❚