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 1c89915297d0f0c93a500be2dfb8ac53bc371de4..bf8b1ae0a1bfc8301a9bd7bbbb042d42d8c5b495 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/$Default$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz
index 6ac2ee49375c8383abdbd49ee318db4d60743b62..022ad2d27d331f0f24d0e91671e23966210f8b78 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.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 573f9896c1421f634ac1494671d60babf5df14fa..4b37bdb1152ec36596733e072ab281d30d430738 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 1dab85d3ee6bc225cec52200f51d559371fb9916..e11b9e79a43c859c1da4ffeaa6baab5ffa7501db 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/$Midpoint.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
index b15b516a6a69e95b3ad2af0d4069640d2c48f016..f03c131da820789cf2e3864e0a489ba9804b9cd6 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.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 d49c48d3553d1fffce76a592b328f9b419d399ff..a108280932a641225023c1f20ece77e258252ef7 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 4ea3894e65019a57eb005d9ace912af6ad94c32b..6c87ea67192b69f18617be0ea0da3e425f4f5c74 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$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz
index fa7d916ce36a2207784a762a6888625cb71b0248..114223d374263e15ccd3d27b4e27aab25ebe3a58 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz
index 706e89af9a856dc78aa350410e66c96c8a95b071..08b96e69ececec2468120093ba7bdde8fcc4ccc9 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz
index e75c297b022be80fddfefcfa067d2e425a91e5ff..a467e2afbf41c1e7dbb81b57dd9bccd9210976d6 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz
index 05d7531d0ec6f0f2fac778abfa1a30082bdfc861..d38587278df425f6c80b39c8203ee3645c79d182 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.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 2d56a5277b71c50cb3c4f67fd8ffcf658ca14efe..85e0225877e29e91348ba044384c93bddf54fcb4 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 6dd9b556cac60a7d100d497b8ea00b418c84c696..4194ad9a114140fcb6c64fb9e711b7b66cf0e034 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 733ad04c42f0fc720bf283e1a3b97879853d6e98..1062d71ff4180da0d295feefa91654e492c0354c 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 8a7089d01ade49a490884818da0dadc9f3ceebd7..31ac251318b6324d8b938908aafebcd8a7008f48 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/$Theory$Parameter$Bug.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz
index eb2ebb70b0fe16878d9da40a13784a12e93c3369..f09ed55d9ceb1e6d251f8facecc5aebe42b3144d 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/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz
index 9eaa82160a954bd1e5527e0b86005f8037e54fb8..23e35212307dd30f5eff206294fcc9974c30f640 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz
index 160ca55d78a4fa4b3f37af2cbb62b3c4ab1d7579..4d18dbfc8c32d7193c548df8f5e8f8ab1f5e6c4d 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/cogwheels.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 d0a790242b7fa63b649ca5a1a57e84dd95e75fd4..9bbe182dc1c9949382d0400870d172efa9cec946 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/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz
index fabc89f483da76ca2092d77ed47dbcb6c09819f2..a822c664abb9b3d34e509dd9a88815b7bdb51abc 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz differ
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/Library/gearbox.mmt.err b/errors/mmt-omdoc/Library/gearbox.mmt.err
index 7a1dca44bcff2c00514b0d1bf0723ca41f107c85..7fdf80f74df50df7d365c12736cc0ed1519ea836 100644
--- a/errors/mmt-omdoc/Library/gearbox.mmt.err
+++ b/errors/mmt-omdoc/Library/gearbox.mmt.err
@@ -50,22 +50,65 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
-    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
-    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
-    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
-    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
-    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
-    <element>FastREPLExtension.run(REPL.scala:52)</element>
-    <element>FastREPL$.run(REPL.scala:44)</element>
-    <element>Test.main(preamble.scala:68)</element>
-    <element>FastREPL.main(REPL.scala)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+    <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+    <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+    <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+    <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:429)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:395)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:411)</element>
+    <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:31)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+    <element>java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1967)</element>
+    <element>java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2308)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:405)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)</element>
+    <element>java.desktop/javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:270)</element>
+    <element>java.desktop/java.awt.Component.processMouseEvent(Component.java:6652)</element>
+    <element>java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3345)</element>
+    <element>java.desktop/java.awt.Component.processEvent(Component.java:6417)</element>
+    <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+    <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5027)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4918)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4547)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4488)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2307)</element>
+    <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2780)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+    <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:976)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchMouseEvent(IdeEventQueue.java:911)</element>
+    <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:840)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:454)</element>
+    <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:773)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:453)</element>
+    <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:822)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:507)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
   </stacktrace>
 </error>
 <error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦y.radius≠0" level="1">
@@ -120,22 +163,65 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
-    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
-    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
-    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
-    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
-    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
-    <element>FastREPLExtension.run(REPL.scala:52)</element>
-    <element>FastREPL$.run(REPL.scala:44)</element>
-    <element>Test.main(preamble.scala:68)</element>
-    <element>FastREPL.main(REPL.scala)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+    <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+    <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+    <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+    <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:429)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:395)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:411)</element>
+    <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:31)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+    <element>java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1967)</element>
+    <element>java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2308)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:405)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)</element>
+    <element>java.desktop/javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:270)</element>
+    <element>java.desktop/java.awt.Component.processMouseEvent(Component.java:6652)</element>
+    <element>java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3345)</element>
+    <element>java.desktop/java.awt.Component.processEvent(Component.java:6417)</element>
+    <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+    <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5027)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4918)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4547)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4488)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2307)</element>
+    <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2780)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+    <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:976)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchMouseEvent(IdeEventQueue.java:911)</element>
+    <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:840)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:454)</element>
+    <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:773)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:453)</element>
+    <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:822)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:507)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
   </stacktrace>
 </error>
 <error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦x.radius≠0" level="1">
@@ -190,22 +276,65 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
-    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
-    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
-    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
-    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
-    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
-    <element>FastREPLExtension.run(REPL.scala:52)</element>
-    <element>FastREPL$.run(REPL.scala:44)</element>
-    <element>Test.main(preamble.scala:68)</element>
-    <element>FastREPL.main(REPL.scala)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+    <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+    <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+    <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+    <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:429)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:395)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:411)</element>
+    <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:31)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+    <element>java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1967)</element>
+    <element>java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2308)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:405)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)</element>
+    <element>java.desktop/javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:270)</element>
+    <element>java.desktop/java.awt.Component.processMouseEvent(Component.java:6652)</element>
+    <element>java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3345)</element>
+    <element>java.desktop/java.awt.Component.processEvent(Component.java:6417)</element>
+    <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+    <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5027)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4918)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4547)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4488)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2307)</element>
+    <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2780)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+    <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:976)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchMouseEvent(IdeEventQueue.java:911)</element>
+    <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:840)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:454)</element>
+    <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:773)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:453)</element>
+    <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:822)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:507)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
   </stacktrace>
 </error>
 <error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦RC.radius≠0" level="1">
@@ -259,22 +388,65 @@
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
     <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
     <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
-    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
-    <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
-    <element>FastREPLExtension.handleLine(REPL.scala:74)</element>
-    <element>FastREPLExtension.$anonfun$run$3(REPL.scala:53)</element>
-    <element>FastREPLExtension.$anonfun$run$3$adapted(REPL.scala:52)</element>
-    <element>scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)</element>
-    <element>scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)</element>
-    <element>scala.collection.AbstractIterator.foreach(Iterator.scala:1279)</element>
-    <element>FastREPLExtension.run(REPL.scala:52)</element>
-    <element>FastREPL$.run(REPL.scala:44)</element>
-    <element>Test.main(preamble.scala:68)</element>
-    <element>FastREPL.main(REPL.scala)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
+    <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
+    <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
+    <element>info.kwarc.mmt.intellij.MMTPluginInterface.handleLine(MMTPlugin.scala:117)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)</element>
+    <element>java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)</element>
+    <element>java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)</element>
+    <element>java.base/java.lang.reflect.Method.invoke(Method.java:566)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror1.jinvokeraw(JavaMirrors.scala:429)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaMethodMirror.jinvoke(JavaMirrors.scala:395)</element>
+    <element>scala.reflect.runtime.JavaMirrors$JavaMirror$JavaVanillaMethodMirror.apply(JavaMirrors.scala:411)</element>
+    <element>info.kwarc.mmt.utils.Reflection$ThisReflectedInstance.method(Reflection.scala:31)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.method(Plugin.scala:111)</element>
+    <element>info.kwarc.mmt.intellij.MMTJar.handleLine(Plugin.scala:122)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.doAction(Shell.scala:39)</element>
+    <element>info.kwarc.mmt.intellij.ui.ShellViewer.actionPerformed(Shell.scala:34)</element>
+    <element>java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1967)</element>
+    <element>java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2308)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:405)</element>
+    <element>java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)</element>
+    <element>java.desktop/javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:270)</element>
+    <element>java.desktop/java.awt.Component.processMouseEvent(Component.java:6652)</element>
+    <element>java.desktop/javax.swing.JComponent.processMouseEvent(JComponent.java:3345)</element>
+    <element>java.desktop/java.awt.Component.processEvent(Component.java:6417)</element>
+    <element>java.desktop/java.awt.Container.processEvent(Container.java:2263)</element>
+    <element>java.desktop/java.awt.Component.dispatchEventImpl(Component.java:5027)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2321)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.retargetMouseEvent(Container.java:4918)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.processMouseEvent(Container.java:4547)</element>
+    <element>java.desktop/java.awt.LightweightDispatcher.dispatchEvent(Container.java:4488)</element>
+    <element>java.desktop/java.awt.Container.dispatchEventImpl(Container.java:2307)</element>
+    <element>java.desktop/java.awt.Window.dispatchEventImpl(Window.java:2780)</element>
+    <element>java.desktop/java.awt.Component.dispatchEvent(Component.java:4859)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:778)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:727)</element>
+    <element>java.desktop/java.awt.EventQueue$4.run(EventQueue.java:721)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:95)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:751)</element>
+    <element>java.desktop/java.awt.EventQueue$5.run(EventQueue.java:749)</element>
+    <element>java.base/java.security.AccessController.doPrivileged(Native Method)</element>
+    <element>java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:85)</element>
+    <element>java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:748)</element>
+    <element>com.intellij.ide.IdeEventQueue.defaultDispatchEvent(IdeEventQueue.java:976)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchMouseEvent(IdeEventQueue.java:911)</element>
+    <element>com.intellij.ide.IdeEventQueue._dispatchEvent(IdeEventQueue.java:840)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$8(IdeEventQueue.java:454)</element>
+    <element>com.intellij.openapi.progress.impl.CoreProgressManager.computePrioritized(CoreProgressManager.java:773)</element>
+    <element>com.intellij.ide.IdeEventQueue.lambda$dispatchEvent$9(IdeEventQueue.java:453)</element>
+    <element>com.intellij.openapi.application.impl.ApplicationImpl.runIntendedWriteActionOnCurrentThread(ApplicationImpl.java:822)</element>
+    <element>com.intellij.ide.IdeEventQueue.dispatchEvent(IdeEventQueue.java:507)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:203)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)</element>
+    <element>java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)</element>
   </stacktrace>
 </error>
 </errors>
diff --git a/narration/DefaultSituationSpace.omdoc b/narration/DefaultSituationSpace.omdoc
index 774145bdeba575a15866550b1f4ba8f50a238884..5c9ef7d20d50c9d42d492299f6d1773584d3f1c7 100644
--- a/narration/DefaultSituationSpace.omdoc
+++ b/narration/DefaultSituationSpace.omdoc
@@ -1,2 +1,2 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#0.0.0:259.10.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace]" target="http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#117.4.0:144.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#0.0.0:300.12.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace]" target="http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#117.4.0:144.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/IntegrationTests/SituationTheory.omdoc b/narration/IntegrationTests/SituationTheory.omdoc
index 1b100fcf3ec5621ceb0304b4780f80405f3d6eca..ed045fe9e54273457a08453c4f5818d560d14873 100644
--- a/narration/IntegrationTests/SituationTheory.omdoc
+++ b/narration/IntegrationTests/SituationTheory.omdoc
@@ -1,2 +1,2 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1753.61.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#271.7.0:291.7.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:2475.84.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#271.7.0:291.7.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Library/gearbox.omdoc b/narration/Library/gearbox.omdoc
index 7a6448a9a110ca2ff454c48804a7b60861877e74..ae65cec770bd3c6da3203bcb2f7a8da3509dbe90 100644
--- a/narration/Library/gearbox.omdoc
+++ b/narration/Library/gearbox.omdoc
@@ -1,2 +1,2 @@
 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2736.75.68"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2739.77.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc
index bb10aba7599ba72d770f36e54f91b7e0336eb65e..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:1072.33.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#70.4.0:198.4.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#628.22.0:723.22.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#725.23.0:745.23.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:1074.34.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#70.4.0:198.4.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#628.22.0:723.22.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#725.23.0:745.23.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/SupplementaryAngles.omdoc b/narration/Scrolls/SupplementaryAngles.omdoc
index aa05b40c5c058594fad7a795c2ec04cccaf1edd8..b5fb88ea673d58f1f1292fc07e06a99e14dcd8e6 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:1612.46.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#78.3.0:245.11.0"/></metadata><scope>\
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#0.0.0:1623.46.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.mmt#78.3.0:245.11.0"/></metadata><scope>\
        \ D
         \
  ________\_________
diff --git a/relational/Scrolls/.rel b/relational/Scrolls/.rel
index 595322539ee56208eed85f28ce52da7db7e763ae..5d4c2a6ea3acf94a471b3688dafd87cfaaa1dfee 100644
--- a/relational/Scrolls/.rel
+++ b/relational/Scrolls/.rel
@@ -2,3 +2,4 @@ document http://mathhub.info/FrameIT/frameworld/Scrolls
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/MiscScrolls.omdoc
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/SupplementaryAngles.omdoc
 Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/Scrolls http://mathhub.info/FrameIT/frameworld/Scrolls/gearbox.omdoc
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
index a9965ba9bfc43f08f620cd373f5d974be9894ff6..f9fa1b075770bb616d2158a68084e3efa8996548 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
@@ -3,6 +3,7 @@ HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://math
 Declares http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace?Root
 theory http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root
 HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?SupplementaryAngles
 Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen
 Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
 Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?Midpoint
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
index ce0b4250c6c19850dd5243e9e3dc615be1750e02..50d95728c641d8489e0823a697d5fecb58e4a10a 100644
--- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
@@ -47,93 +47,229 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechec
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
-constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
-constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
-constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Strings?string?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?first_view
-HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view ☞frameworld:?OppositeLen/Problem
+HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
 HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
 view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view
-HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root ☞frameworld:?OppositeLen/Problem
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
-constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
-constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
-constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
+HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace?Derived1
+theory http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1 http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1 http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1 http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Trigonometry?tan?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1 http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?first_pushout_view
+HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution
+HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1
+view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view
+HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1 http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?deducedLineCA?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[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/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/first_pushout_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Solution]/deducedLineCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1 http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1?second_view
+HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
+HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1
+view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view
+HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1 http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/B?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem]/C?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?OppositeLen/Problem]/distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleB?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_AngleAtB]/angleB?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngleC?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Derived1/second_view?[http://mathhub.info/FrameIT/frameworld?TriangleProblem_RightAngleAtC]/rightAngleC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
index f66643109829b8fb3e01fb30d61a678b6a6a2b59..7ad9610d93a4894788dafcc78b4b9e12c577145a 100644
--- a/source/DefaultSituationSpace.mmt
+++ b/source/DefaultSituationSpace.mmt
@@ -4,6 +4,7 @@ fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
 
 theory DefaultSituationSpace =
     theory Root =
+        include ?SupplementaryAngles ❙
         include ?OppositeLen ❙
         include ?AngleSum ❙
         include ?Midpoint ❙
diff --git a/source/Scrolls/SupplementaryAngles.mmt b/source/Scrolls/SupplementaryAngles.mmt
index ebadc26333279d11a0643114ca5189773e589fa8..e6e3184849251d68dbb65f7c42250f505089ccd2 100644
--- a/source/Scrolls/SupplementaryAngles.mmt
+++ b/source/Scrolls/SupplementaryAngles.mmt
@@ -32,7 +32,7 @@ theory SupplementaryAngles =
     ❚
 
     theory Solution =
-        meta ?MetaAnnotations?label "AngleSum" ❙
+        meta ?MetaAnnotations?label "SupplementaryAngles" ❙
         meta ?MetaAnnotations?description "Supplementary angles add up to 180 degree " ❙
 
         include ?SupplementaryAngles/Problem ❙