diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
index 71042ec64dcd2d628c4fbfd128844e392f662811..8c0bb2a711a6a9f23e9f1848a24ec695edce7d65 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
index afd90f697c89d845f7f3ccecbc0fcae9f7029389..5815e8625d0828250cbf7bed52798060475429af 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz
index 70d82f162407d7e4972b797ab9c3dcb0d644453e..1cc3cf5cc1b3c9e1626d798a72799a658eed5c9d 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
index a5a882abc1cfad4cc35f3263d5f9e48ee0e01964..eac5cab4a80292619b1a927cede9fcd886f5259e 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz
index 7d6ec3931c4e4efa54e226fa32d1cada84eec001..e0161fc290577fe9d4d7fa83b675bac34fe83237 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz differ
diff --git 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
index c2c96a06e1e46ffb8de29265790a98cc012b8752..5511dae393b2b5d1a5bf2f7b19a975942bb325a5 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz differ
diff --git 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
index c549a1d9ed0db2f21638365c291c43d0c72b5187..9cb883cfbebb09913ded77093cb43307a1c28401 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz
index 07f03001d8caf688406f7da7c9ffbf5046c9e1fc..9a99fa637efac2db63ae26a46b0eec372ea605ce 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz
index 0c9271de6374ee96b539d282b4fa934e1ae50c8a..d4d8dc7fc1aed68d20f9a7a09d8171bfebc3fdbd 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz
index ffd52177d18236516202e94ceb1a50f7decec5c2..70e687eb8d08c92c95fcca20b1ae0cf4082324e3 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz
index 092c04b3d2b0ff1c2ad9d77527cac70376943286..88839abfc4fd6c90d2d1ea8be11e86424da0a226 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.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 b50e33a2fb6a16b5bd16f65b081f013d5312e3ab..8e690f6dd6a2a7823f8d660cc1314e7eb65140c2 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/$Theory$Parameter$Bug.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz
index a6ef23783c077c095912fedaaadec97045162bd4..42545b9f63fc964af48ccf82b9330e743136817f 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz
index f8a9d80bae60e1929e3dd5d6d1f7a5eb738b3229..23ae774e6648a7f516d796aea2f89d83a69f270a 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz differ
diff --git a/errors/mmt-omdoc/IntegrationTests/ExpectedTypeTests.mmt.err b/errors/mmt-omdoc/IntegrationTests/ExpectedTypeTests.mmt.err
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a003a310ddaac2945e140ceaaaa6d7e3db90d6b4 100644
--- a/errors/mmt-omdoc/IntegrationTests/ExpectedTypeTests.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/ExpectedTypeTests.mmt.err
@@ -0,0 +1,2 @@
+<errors>
+</errors>
diff --git a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a003a310ddaac2945e140ceaaaa6d7e3db90d6b4 100644
--- a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
@@ -0,0 +1,2 @@
+<errors>
+</errors>
diff --git a/errors/mmt-omdoc/IntegrationTests/thy-parameter-bug.mmt.err b/errors/mmt-omdoc/IntegrationTests/thy-parameter-bug.mmt.err
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a003a310ddaac2945e140ceaaaa6d7e3db90d6b4 100644
--- a/errors/mmt-omdoc/IntegrationTests/thy-parameter-bug.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/thy-parameter-bug.mmt.err
@@ -0,0 +1,2 @@
+<errors>
+</errors>
diff --git a/errors/mmt-omdoc/MetaTheories.mmt.err b/errors/mmt-omdoc/MetaTheories.mmt.err
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a003a310ddaac2945e140ceaaaa6d7e3db90d6b4 100644
--- a/errors/mmt-omdoc/MetaTheories.mmt.err
+++ b/errors/mmt-omdoc/MetaTheories.mmt.err
@@ -0,0 +1,2 @@
+<errors>
+</errors>
diff --git a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a003a310ddaac2945e140ceaaaa6d7e3db90d6b4 100644
--- a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
+++ b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err
@@ -0,0 +1,2 @@
+<errors>
+</errors>
diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc
index f1014194a3bc36dcc4fee92df9d0289098c6a94a..a75d096ac0d47212c0f5963561f4ffb33343746b 100644
--- a/narration/MetaTheories.omdoc
+++ b/narration/MetaTheories.omdoc
@@ -1,2 +1,2 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0: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
+<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
diff --git a/narration/Scrolls/SupplementaryAngles.omdoc b/narration/Scrolls/SupplementaryAngles.omdoc
index c5e6d154b5454d3d7989e456697b3de38e4cea8e..bee3fe30604ae88df5104330ac54e16dacdf9905 100644
--- a/narration/Scrolls/SupplementaryAngles.omdoc
+++ b/narration/Scrolls/SupplementaryAngles.omdoc
@@ -1,5 +1,5 @@
 <?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:1632.45.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#79.4.0:246.12.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:1620.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#79.4.0:246.12.0"/></metadata><scope>\
        \ D
         \
  ________\_________
diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc
index 068c49e7bac7999bcdfd1b22090ad10b185829a5..b9aa7bc702b1141583c0d68973acbdeaaf412c2b 100644
--- a/narration/Scrolls/TriangleScrolls.omdoc
+++ b/narration/Scrolls/TriangleScrolls.omdoc
@@ -1,5 +1,5 @@
 <?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: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
+<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:4637.131.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#579.20.0:735.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#462.20.0:618.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#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
+   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#620.23.0:659.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#892.32.0:906.32.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#2197.66.0:2214.66.17"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/IntegrationTests/.rel b/relational/IntegrationTests/.rel
index 330e88ba2ab2d4585f6959034a7fb10832063b57..a760cb966edace2076fc3f112a3a59b677939311 100644
--- a/relational/IntegrationTests/.rel
+++ b/relational/IntegrationTests/.rel
@@ -2,3 +2,4 @@ document http://mathhub.info/FrameIT/frameworld/IntegrationTests
 Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapsTests.omdoc
 Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc
 Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests http://mathhub.info/FrameIT/frameworld/IntegrationTests/thy-parameter-bug.omdoc
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
index f1cf578e33ff9de9b141901f54e2cb213f5eb2ec..531b143ac24cee9e7fd92444517a5ca1f84cac60 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel
@@ -1,63 +1,63 @@
 theory http://mathhub.info/FrameIT/frameworld?AngleSum
 HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/FrameIT/frameworld?AngleSum?AngleSum_Problem
-theory http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem
-HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC
-constant http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC
-constant http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/FrameIT/frameworld?AngleSum?AngleSum_Solution
-theory http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution
-HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem
-Declares http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA
-constant http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleABC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Problem?angleBAC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-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://cds.omdoc.org/urtheories?Strings?string?type
+Declares http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/FrameIT/frameworld?AngleSum?Problem
+theory http://mathhub.info/FrameIT/frameworld?AngleSum/Problem
+HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem
+Declares http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC
+constant http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+Declares http://mathhub.info/FrameIT/frameworld?AngleSum/Problem http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC
+constant http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+Declares http://mathhub.info/FrameIT/frameworld?AngleSum http://mathhub.info/FrameIT/frameworld?AngleSum?Solution
+theory http://mathhub.info/FrameIT/frameworld?AngleSum/Solution
+HasMeta http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.info/FrameIT/frameworld?AngleSum/Problem
+Declares http://mathhub.info/FrameIT/frameworld?AngleSum/Solution http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA
+constant http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleABC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?AngleSum/Problem?angleBAC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
index 98a5ed6ba63fd4f6af04ecf2a911081d8da3c0e9..e536a64362cc94b10b164c9d8150400f495672b9 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel
@@ -3,6 +3,7 @@ untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?descripti
 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
+untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?description_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
@@ -16,3 +17,5 @@ Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.i
 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
+Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/FrameIT/frameworld?MetaAnnotations?description_verbalization_of
+constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?description_verbalization_of
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
index da2b8a6cf5bef00d2593566570fd4c196c7fedb2..a678981ac33eed8539f0506e5f5dd93bf10c14cb 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel
@@ -1,61 +1,61 @@
 theory http://mathhub.info/FrameIT/frameworld?OppositeLen
 HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Declares http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/FrameIT/frameworld?OppositeLen?OppositeLen_Problem
-theory http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem
-HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem
-Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC
-constant http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC
-constant http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/FrameIT/frameworld?OppositeLen?OppositeLen_Solution
-theory http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution
-HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem
-Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA
-constant http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Trigonometry?tan?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?distanceBC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Problem?angleABC?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
-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://cds.omdoc.org/urtheories?Strings?string?type
+Declares http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/FrameIT/frameworld?OppositeLen?Problem
+theory http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
+HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem
+Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC
+constant http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC
+constant http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+Declares http://mathhub.info/FrameIT/frameworld?OppositeLen http://mathhub.info/FrameIT/frameworld?OppositeLen?Solution
+theory http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution
+HasMeta http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
+Declares http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA
+constant http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?distanceBC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Trigonometry?tan?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem?angleABC?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel
index daf360c33949aa0fcfe7863c707232b08ea02f35..4d92d994ade885b0bde8e5c035e0d84105aad622 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.rel
@@ -1,101 +1,101 @@
 theory http://mathhub.info/FrameIT/frameworld?SupplementaryAngles
 HasMeta http://mathhub.info/FrameIT/frameworld?SupplementaryAngles http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles http://mathhub.info/FrameIT/frameworld?SupplementaryAngles?SupplementaryAngles_Problem
-theory http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem
-HasMeta http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?D
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?D
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?D?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?D?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?L
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?L
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?L?type
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?L?type
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?L?type
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?D?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles http://mathhub.info/FrameIT/frameworld?SupplementaryAngles?SupplementaryAngles_Solution
-theory http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution
-HasMeta http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Includes http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem
-Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC
-constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?D?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?angleABD?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?D?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Problem?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/SupplementaryAngles_Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles http://mathhub.info/FrameIT/frameworld?SupplementaryAngles?Problem
+theory http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem
+HasMeta http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/MitM/core/geometry?Geometry/Common?onLine?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C_on_L?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?L?type
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles http://mathhub.info/FrameIT/frameworld?SupplementaryAngles?Solution
+theory http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution
+HasMeta http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem
+Declares http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC
+constant http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?D?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Problem?angleABD?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld?SupplementaryAngles/Solution?angleDBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel
index ae911a900540c51ba72c5adb106fb22966f65f05..da8a1a1fae224d3f48f98c6e1a2369ea27d65bd1 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.rel
@@ -38,4 +38,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://mathhub.info/MitM/Foundation?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?definition http://cds.omdoc.org/urtheories?Strings?string?type
diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index cb2ec21951496c54043f153d85cf917ec98436c6..d4537efa5248828c8aa8f708e8da778e729280c7 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -12,8 +12,12 @@ theory MetaAnnotations =
     problemTheory ❙
     solutionTheory❙
 
-    /T example: lverb ?fact "default text" ❙
+    /T Example usages:
+         - `lverb A`, where A refers to a symbol
+         - `lverb A B`, a shorthand for `concat (lverb A) (lverb B)`; works for arbitrary number of arguments
+    ❙
     label_verbalization_of # lverb ❙
+    description_verbalization_of # dverb ❙
 ❚
 
 /T The meta theory to use for situation theories, scroll problem, and scroll solution theories ❚
diff --git a/source/Scrolls/SupplementaryAngles.mmt b/source/Scrolls/SupplementaryAngles.mmt
index 743a08c1a3609d60e49e70b4d832ccabc52328d7..1f711821a298bcc7c4cf14dad5aadfc34c7b71e7 100644
--- a/source/Scrolls/SupplementaryAngles.mmt
+++ b/source/Scrolls/SupplementaryAngles.mmt
@@ -12,35 +12,36 @@ A         B        C
 The scroll encodes "angle ABD + angle DBC = 180°", or rather, "angle DBC = 180° - angle ABD"
 ❚
 theory SupplementaryAngles =
-    theory SupplementaryAngles_Problem =
-        A: point ❘ meta ?MetaAnnotations?label "Point A" ❙
-        B: point ❘ meta ?MetaAnnotations?label "Point B" ❙
-        C: point ❘ meta ?MetaAnnotations?label "Point C" ❙
-        D: point ❘ meta ?MetaAnnotations?label "Point D" ❙
+    theory Problem =
+        A: point ❘ meta ?MetaAnnotations?label "A" ❙
+        B: point ❘ meta ?MetaAnnotations?label "B" ❙
+        C: point ❘ meta ?MetaAnnotations?label "C" ❙
+        D: point ❘ meta ?MetaAnnotations?label "D" ❙
 
-        L: line ❘ meta ?MetaAnnotations?label "Line L"❙
-        A_on_L : ⊦ A on L ❘ meta ?MetaAnnotations?label "A on L"❙
-        B_on_L : ⊦ B on L ❘ meta ?MetaAnnotations?label "B on L"❙
-        C_on_L : ⊦ C on L ❘ meta ?MetaAnnotations?label "C on L"❙
+        L: line ❘ meta ?MetaAnnotations?label "L"❙
+        A_on_L : ⊦ A on L ❘ meta ?MetaAnnotations?label s"${lverb A} ∈ ${lverb L}"❙
+        B_on_L : ⊦ B on L ❘ meta ?MetaAnnotations?label s"${lverb B} ∈ ${lverb L}"❙
+        C_on_L : ⊦ C on L ❘ meta ?MetaAnnotations?label s"${lverb C} ∈ ${lverb L}"❙
 
         angleABD
             : Σ α: ℝ. ⊦ ( ∠ A,B,D ) ≐ α ❘
-            meta ?MetaAnnotations?description "Angle between A, B, and D"
+            meta ?MetaAnnotations?label s"∠${lverb A B D}"
         ❙
     ❚
 
-    theory SupplementaryAngles_Solution =
+    theory Solution =
         meta ?MetaAnnotations?label "AngleSum" ❙
-        meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/SupplementaryAngles_Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?SupplementaryAngles/SupplementaryAngles_Solution ❙
-        meta ?MetaAnnotations?description "Supplementary Angles add up to 180 degree " ❙
+        meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/Problem ❙
+        meta ?MetaAnnotations?solutionTheory ?SupplementaryAngles/Solution ❙
+        meta ?MetaAnnotations?description "Supplementary angles add up to 180 degree " ❙
 
-        include ?SupplementaryAngles/SupplementaryAngles_Problem ❙
+        include ?SupplementaryAngles/Problem ❙
 
         angleDBC
             : Σ γ: ℝ. ⊦ ( ∠ D,B,C ) ≐ γ ❘
             = ⟨180.0 - (πl angleABD), sketch "By some theorem"⟩ ❘
-            meta ?MetaAnnotations?description "The deduced angle by calculating 180° - α"
+            meta ?MetaAnnotations?label s"∠${lverb D B C}" ❘
+            meta ?MetaAnnotations?description s"The deduced angle by calculating 180° - ${lverb angleABD}"
         ❙
     ❚
 ❚
\ No newline at end of file
diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt
index 71f4c89681ee4ca8ccff471823f4a6b0371dbd68..b45c20aa346ee25868b0628c453636a21a6af0b0 100644
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -13,9 +13,9 @@ fixmeta ?FrameworldMeta ❚
   (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)
 ❚
 theory TriangleScroll_GeneralProblem =
-    A: point ❘ meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?A "A" ❙
-    B: point ❘ meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?B "B"❙
-    C: point ❘ meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?C "C"❙
+    A: point ❘ meta ?MetaAnnotations?label "A" ❙
+    B: point ❘ meta ?MetaAnnotations?label "B"❙
+    C: point ❘ meta ?MetaAnnotations?label "C"❙
 ❚
 
 /T A blueprint problem theory for triangle scrolls that require a right angle
@@ -25,75 +25,82 @@ theory TriangleScroll_RightAngledProblem =
     include ?TriangleScroll_GeneralProblem ❙
     rightAngleBCA
         : ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘
-        meta ?MetaAnnotations?description "Right angle at C"
+        meta ?MetaAnnotations?label s"∟${lverb C}" ❘
+        meta ?MetaAnnotations?description s"Right angle at ${lverb C}"
     ❙
 ❚
 
 theory AngleSum =
-    theory AngleSum_Problem =
+    theory Problem =
         include ?TriangleScroll_GeneralProblem ❙
 
         angleBAC
             : Σ α: ℝ. ⊦ ( ∠ B,A,C ) ≐ α ❘
-            meta ?MetaAnnotations?description "Angle α at A"
+            meta ?MetaAnnotations?label s"∠${lverb B A C}" ❘
+            meta ?MetaAnnotations?description s"Angle at ${lverb A}"
         ❙
 
         angleABC
             : Σ β: ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
-            meta ?MetaAnnotations?label "Angle β at B"
+            meta ?MetaAnnotations?label s"∠${lverb A B C}" ❘
+            meta ?MetaAnnotations?description s"Angle at ${lverb B}"
         ❙
     ❚
 
-    theory AngleSum_Solution =
+    theory Solution =
         meta ?MetaAnnotations?label "AngleSum" ❙
-        meta ?MetaAnnotations?problemTheory ?AngleSum/AngleSum_Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?AngleSum/AngleSum_Solution ❙
-        meta ?MetaAnnotations?description "Given a triangle ABC and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°" ❙
+        meta ?MetaAnnotations?problemTheory ?AngleSum/Problem ❙
+        meta ?MetaAnnotations?solutionTheory ?AngleSum/Solution ❙
+        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} and two known angles, we can deduce the missing angle by the sum of interior angles in triangles always being 180°" ❙
 
-       include ?AngleSum/AngleSum_Problem ❙
+       include ?AngleSum/Problem ❙
 
         angleBCA
             : Σ γ: ℝ. ⊦ ( ∠ B,C,A ) ≐ γ ❘
             = ⟨180.0 - (πl angleBAC) - (πl angleABC), sketch "By sum of interior angles = 180° in triangles"⟩ ❘
-            meta ?MetaAnnotations?description "The deduced angle by calculating 180° - α - β"
+            meta ?MetaAnnotations?label s"∠${lverb B C A}" ❘
+            meta ?MetaAnnotations?description s"The deduced angle by calculating 180° - ${lverb angleBAC} - ${lverb angleABC}"
         ❙
     ❚
 ❚
 
 theory OppositeLen =
-    theory OppositeLen_Problem =
+    theory Problem =
         include ?TriangleScroll_RightAngledProblem ❙
     
         distanceBC
             : Σ x:ℝ . ⊦ ( d- B C ) ≐ x ❘
-            meta ?MetaAnnotations?label "Length of leg BC"
+            meta ?MetaAnnotations?label s"${lverb B C}" ❘
+            meta ?MetaAnnotations?description s"Length of leg ${lverb B C}"
         ❙
     
         angleABC
             : Σ a:ℝ . ⊦ ( ∠ A,B,C ) ≐ a ❘
-            meta ?MetaAnnotations?label "Angle at B"
+            meta ?MetaAnnotations?label s"∠${lverb A B C}" ❘
+            meta ?MetaAnnotations?description s"Angle at ${lverb B}"
         ❙
     ❚
     
-    theory OppositeLen_Solution =
+    theory Solution =
+        include ?OppositeLen/Problem ❙
+
         meta ?MetaAnnotations?label "OppositeLen" ❙
-        meta ?MetaAnnotations?problemTheory ?OppositeLen/OppositeLen_Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?OppositeLen/OppositeLen_Solution ❙
-        meta ?MetaAnnotations?description s"Given a triangle ${lverb ?TriangleScroll_GeneralProblem?A "A"}${lverb ?TriangleScroll_GeneralProblem?B "B"}${lverb ?TriangleScroll_GeneralProblem?C "C"} right angled at ${lverb ?TriangleScroll_GeneralProblem?C "C"}, the distance ${lverb ?TriangleScroll_GeneralProblem?A "A"}${lverb ?TriangleScroll_GeneralProblem?B "B"} can be computed from the angle at ${lverb ?TriangleScroll_GeneralProblem?B "B"} and the distance ${lverb ?TriangleScroll_GeneralProblem?B "B"}${lverb ?TriangleScroll_GeneralProblem?C "C"}" ❙
-    
-        include ?OppositeLen/OppositeLen_Problem ❙
+        meta ?MetaAnnotations?problemTheory ?OppositeLen/Problem ❙
+        meta ?MetaAnnotations?solutionTheory ?OppositeLen/Solution ❙
+        meta ?MetaAnnotations?description s"Given a triangle ${lverb A B C} right angled at ${lverb C}, the distance ${lverb A B} can be computed from the angle at ${lverb B} and the distance ${lverb B C}" ❙
     
         deducedLineCA
             : Σ x:ℝ . ⊦ (d- C A) ≐ x ❘
             = ⟨(tan (πl angleABC)) ⋅ (πl distanceBC), sketch "OppositeLen Scroll"⟩ ❘
-            meta ?MetaAnnotations?description "The deduced length of the line CA"
+            meta ?MetaAnnotations?label s"${lverb C A}" ❘
+            meta ?MetaAnnotations?description s"The deduced length of the line ${lverb C A}"
         ❙
     ❚
 ❚
 
 // Doesn't typecheck, not sure why ❚
 // theory Pythagoras =
-    theory Pythagoras_Problem =
+    theory Problem =
         include ?TriangleScroll_RightAngledProblem ❙
     
         distanceAC
@@ -107,13 +114,13 @@ theory OppositeLen =
         ❙
     ❚
     
-    // theory Pythagoras_Solution =
+    // theory Solution =
         meta ?MetaAnnotations?label "Pythagoras" ❙
-        meta ?MetaAnnotations?problemTheory ?Pythagoras/Pythagoras_Problem ❙
-        meta ?MetaAnnotations?solutionTheory ?Pythagoras/Pythagoras_Solution ❙
+        meta ?MetaAnnotations?problemTheory ?Pythagoras/Problem ❙
+        meta ?MetaAnnotations?solutionTheory ?Pythagoras/Solution ❙
         meta ?MetaAnnotations?description "Given a ABC right-angled at C and lengths of both legs, we can compute the length of the hypotenuse via Pythagora's theorem" ❙
 
-        include ?Pythagoras/Pythagoras_Problem ❙
+        include ?Pythagoras/Problem ❙
 
         deducedHypotenuse
             : Σ x:ℝ. ⊦ (d- A B) ≐ x ❘