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
new file mode 100644
index 0000000000000000000000000000000000000000..bd614b70d5e5f6096c4d925332ff03922e454b9e
Binary files /dev/null and b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz differ
diff --git a/errors/mmt-omdoc/DefaultSituationSpace.mmt.err b/errors/mmt-omdoc/DefaultSituationSpace.mmt.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/narration/DefaultSituationSpace.omdoc b/narration/DefaultSituationSpace.omdoc
new file mode 100644
index 0000000000000000000000000000000000000000..774145bdeba575a15866550b1f4ba8f50a238884
--- /dev/null
+++ b/narration/DefaultSituationSpace.omdoc
@@ -0,0 +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
diff --git a/relational/DefaultSituationSpace.rel b/relational/DefaultSituationSpace.rel
new file mode 100644
index 0000000000000000000000000000000000000000..9fa3f6ac822988a36848a0817d8b26bcab38fee3
--- /dev/null
+++ b/relational/DefaultSituationSpace.rel
@@ -0,0 +1,2 @@
+document http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
new file mode 100644
index 0000000000000000000000000000000000000000..a9965ba9bfc43f08f620cd373f5d974be9894ff6
--- /dev/null
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
@@ -0,0 +1,8 @@
+theory http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace
+HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+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?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/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
new file mode 100644
index 0000000000000000000000000000000000000000..f66643109829b8fb3e01fb30d61a678b6a6a2b59
--- /dev/null
+++ b/source/DefaultSituationSpace.mmt
@@ -0,0 +1,11 @@
+namespace http://mathhub.info/FrameIT/frameworld âš
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
+
+theory DefaultSituationSpace =
+ theory Root =
+ include ?OppositeLen â™
+ include ?AngleSum â™
+ include ?Midpoint â™
+ âš
+âš
diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt
index bc4e894059eaf8a2fa0665fee2d8d16c30fd0f31..4258dc07b611d6b23fed9e7c54cf29a89936125b 100644
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -75,7 +75,11 @@ theory SituationSpace =
theory PushedOutSituationTheory =
include ?SituationSpace/RootSituationTheory â™
- c: type ☠= b â™
+ c: type â™
q = p â™
+
+ view w : ?MyScroll/Problem -> ?SituationSpace/PushedOutSituationTheory =
+ a = c â™
+ âš
âš
âš
\ No newline at end of file
diff --git a/source/examples/misc.mmt b/source/examples/misc.mmt
deleted file mode 100644
index 748ee87156cfed31f51569b8f43ec6480b5331c9..0000000000000000000000000000000000000000
--- a/source/examples/misc.mmt
+++ /dev/null
@@ -1,81 +0,0 @@
-namespace http://mathhub.info/FrameIT/frameworld/examples âš
-
-// theory Examples : http://mathhub.info/FrameIT/frameworld?SituationTheoryMeta =
- A: point ☠= ⟨1.0, 2.0, 3.0⟩â™
- B: point ☠= ⟨4.0, 5.0, 6.0⟩â™
-
- // this doesn't typecheck due to an MMT bug -- iirc not even Dennis knows what is going on â™
- line_AB: line_type ☠= lineOf A B â™
-
- // The measuring tape gadget should produce this fact â™
- measured_distance: ⊦ ( ( d- A B) ≠42 ) ☠= sketch "measured by Unity" â™
-
- // Below are JSON representations of the above declarations that serve to help build the Unity side â™
-
- // JSON representation for A: {
- "tp": {
- "kind": "OMS",
- "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point"
- },
- "df": {
- "kind": "OMA",
- "applicant": {
- "kind": "OMS",
- "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple"
- },
- "arguments": [
- {"kind": "OMF", "float": 1.0},
- {"kind": "OMF", "float": 2.0},
- {"kind": "OMF", "float": 3.0}
- ]
- }
- } â™
-
- // JSON representation of line_AB: {
- "tp": {
- "kind": "OMS",
- "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type",
- },
- "df": {
- "kind": "OMA",
- "applicant": {
- "kind": "OMS",
- "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?lineOf"
- },
- "arguments": [
- {"kind": "OMS", "uri": "http://mathhub.info/FrameIT/frameworld/examples?Examples?A"},
- {"kind": "OMS", "uri": "http://mathhub.info/FrameIT/frameworld/examples?Examples?B"},
- ]
- }
- } â™
-
- // JSON representation for measured_distance: {
- "tp": {
- "kind": "OMA",
- "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/Foundation?Logic?ded"},
- "arguments": [{
- "kind": "OMA",
- "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/Foundation?Logic?eq"},
- "arguments": [
- {
- "kind": "OMA",
- "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?metric"},
- "arguments": [
- {"kind": "OMS", "uri": "<uri to situation theory, i.e. Examples here>?A"},
- {"kind": "OMS", "uri": "<uri to situation theory, i.e. Examples here>?B"}
- ]
- },
- {"kind": "OMF", "float": 42}
- ],
- }]
- },
- "df": {
- "kind": "OMA",
- "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch"},
- "arguments": [
- {"kind": <copy contents of tp here>},
- {"kind": "OMSTR", "string": "measured by Unity"}
- ]
- }
- }â™
-âš