From 7c958af74ed45fa1e4f098e498dbc25c8439f3da Mon Sep 17 00:00:00 2001
From: SESch93 <john.schihada@hotmail.com>
Date: Wed, 28 Apr 2021 12:16:27 +0200
Subject: [PATCH] Added SupplementaryAngles-Scroll to DefaultSituationSpace

---
 .../FrameIT/frameworld/$Angle$Sum.omdoc.xz    | Bin 1968 -> 1936 bytes
 .../$Default$Situation$Space.omdoc.xz         | Bin 588 -> 604 bytes
 .../frameworld/$Frameworld$Meta.omdoc.xz      | Bin 720 -> 716 bytes
 .../frameworld/$Meta$Annotations.omdoc.xz     | Bin 880 -> 876 bytes
 .../FrameIT/frameworld/$Midpoint.omdoc.xz     | Bin 1724 -> 1684 bytes
 .../FrameIT/frameworld/$Opposite$Len.omdoc.xz | Bin 2184 -> 2152 bytes
 .../frameworld/$Supplementary$Angles.omdoc.xz | Bin 2288 -> 2260 bytes
 .../frameworld/$Triangle$Problem.omdoc.xz     | Bin 648 -> 644 bytes
 .../$Triangle$Problem_$Angle$At$A.omdoc.xz    | Bin 1300 -> 1280 bytes
 .../$Triangle$Problem_$Angle$At$B.omdoc.xz    | Bin 1160 -> 1140 bytes
 ...riangle$Problem_$Right$Angle$At$C.omdoc.xz | Bin 1280 -> 1260 bytes
 .../$Close$Gaps$Test_$Codomain.omdoc.xz       | Bin 1096 -> 1092 bytes
 .../$Close$Gaps$Test_$Terms$Notepad.omdoc.xz  | Bin 1008 -> 980 bytes
 .../$Expected$Type$Test_$Codomain.omdoc.xz    | Bin 884 -> 860 bytes
 .../$Expected$Type$Test_$Domain.omdoc.xz      | Bin 908 -> 904 bytes
 .../$Theory$Parameter$Bug.omdoc.xz            | Bin 1004 -> 1000 bytes
 .../$Situation$Space.omdoc.xz                 | Bin 1916 -> 3128 bytes
 .../LoViVo/gearbox/cogwheels.omdoc.xz         | Bin 1188 -> 1180 bytes
 .../LoViVo/gearbox/gearbox.omdoc.xz           | Bin 2560 -> 2532 bytes
 .../LoViVo/gearbox/temp.omdoc.xz              | Bin 1324 -> 1308 bytes
 .../IntegrationTests/SituationTheory.mmt.err  |   2 +
 errors/mmt-omdoc/Library/gearbox.mmt.err      | 300 +++++++++++++----
 narration/DefaultSituationSpace.omdoc         |   2 +-
 .../IntegrationTests/SituationTheory.omdoc    |   2 +-
 narration/Library/gearbox.omdoc               |   2 +-
 narration/MetaTheories.omdoc                  |   2 +-
 narration/Scrolls/SupplementaryAngles.omdoc   |   2 +-
 relational/Scrolls/.rel                       |   1 +
 .../frameworld/$Default$Situation$Space.rel   |   1 +
 .../$Situation$Space.rel                      | 310 +++++++++++++-----
 source/DefaultSituationSpace.mmt              |   1 +
 source/Scrolls/SupplementaryAngles.mmt        |   2 +-
 32 files changed, 470 insertions(+), 157 deletions(-)

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
GIT binary patch
delta 69
zcmdnMKY@RO45R->S!;F+#oo(jH|(3Rb9;E%f`-gS);=BWXXbGX3?C0&v{3g`+RwoF
Zn(yc{Muu5Tj9)h%N&n5n00b<NQ2@%}8g&2w

delta 101
zcmV-r0Gj`h53moA906~!9XkhDIcMNa0-bU^%DNW%;|RMmAH4KsCP+SD6<?J}!tgtq
z=qOuNKhQs%M`+zf*@t;C3_{1(?KA)Y@xswKCr%>200D~+#pVG3a3qz$vBYQl0ssI2
H00dcDQdcPG

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
GIT binary patch
delta 392
zcmV;30eAk)1l$CW83YWJ0vVAV$bVjKWP+bK{trV**3VR$W_q<;JMi0c%pFYHfpYf?
zju76PY*+o607*+|+$(n4jYTo*CZ19JyvsbDvK5BiSQJq|JMU_+>B7BQ;q9J-vhic^
z5M+yS2zo#L15iLJ8WX(I5^8|?vmlTxoDLQ7Bf6fZ^Uza($19T(vPr&C?tj&f&Fv}i
z%WT?)y@fgUaji|ZjJiA@i?W-v-u75r6zEpx{+WRQc-LakVS;p$P*y_1L$hCK<ujp7
zzsR9Twj~6J|7l-0jp4>b*&MT}=C|~O)J(y_xH^{|aF&=dbfh0WACf>}5eC{{GurCC
zRUn(i%i!orudZqNYK8fE9eKaODlRU~`sRYk8r4-egsTHrJ^%3QFsu#>X=H$nGE|@$
zLi8fKudLdYy9p`Cc~B}f0Q#)5&a22E2x_^=pE1vXXJmw6!?kEZ{Zp>P(BUJ=F5mzF
m0000H8=Nx}yL*%X0ks5`82|vXdAsGY#Ao{g000001X)^g(!aj|

delta 376
zcmV-;0f+wF1k41G83YQA0t}HI$bVd}g&_tG{{ma3^C*nGXhIzwB#ntE$mHqrDGc&{
z-U+}@DFrar;sF^5!$sF31}usJ0Nl&0?PWF0>2`rK$eZ+LXwTev!x;Lr3SLS&wcvhz
zu*PTb7-vL&H?tCYzzEe0hX-fC;)3qntdL8*W#U#I(VX6~_P&6t3HxInqkoy4Yc)Qo
z!sAIBu%mTpg@}az(R<ipL0}|j^5EoTJaE%0I|UR*;(fj3q8CRwcSjrEx4PsXsjAR>
z0r8aoJAu-7ta0&5CeDD4B)tvjd0Fx>>s2m0Rhr+s6#ysv!{0$!q=BALrE51QvU!WN
z#wW9QK9>T~wLI)<GPUq+8fnIN-zh#SC%WIR5n50JSE(s;{)XhqOKO;_lRYe}ZvbVQ
zlZ`bqOO3f7V(FChmSp#G3k<V^DIit{39u5IU}LT;HPo@^+}HpWv*OBkK7P~y0jLCy
W6#xJYLGjeF#Ao{g000001X)^c0<n$&

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
GIT binary patch
delta 60
zcmcb>dWLm^3}fd;*#;*4>5Si2vUl~Yez;be0SNAhGnCaGS-q5jaVhIZB?g8)7Uk|6
OkEH)*0!gw&Mgah*7!>~i

delta 64
zcmX@ZdVzI<3}fF$*#;)#Y1!N^N9W6!*z9s&Ja1Q|0RscW9dU-Tx+ANXGBB=U{iwvi
UklCfUZR3&j-%LO`2A0Su0Q6iILI3~&

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
GIT binary patch
delta 59
zcmeys_J(bO45Ri&Sw&{O`3!u8hi+v$d)~cY&cLuzdC!6ab3R2dFdk?7F2%rblKqF*
P#v|#!nHYe8B{B*Cs<ajo

delta 63
zcmV-F0Kot32Ji-u904z}9U%iUp8xt)$DKaK<iddgA`id-005~Yyr96G@>l=?%Lexv
V006SbIz6$(XZr#G00004Sz1Mo7={1<

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
GIT binary patch
delta 62
zcmdnPJB4?G3}fI%SvNMry_!Y|j1h<2mG5sa4`2X-=&vdYKNS+MGcdm8S$LX}fq~ug
P?#3hOznMUiERj(FgtZhG

delta 102
zcmV-s0Ga=k4ZIDI907W<9YzLOw*~3Z=%#1f&u;to=r5i_F=f?sI*?gKK<UDuA{_%F
zK5Pj`ThLXmTrf6RK*up|EZSoMwJHDr09*AWAo(C+*8l;Q4WY{c0J77}fw9DA`vL#}
I000D8TF^o%G5`Po

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
GIT binary patch
delta 63
zcmeAWd?7GFhEZ*!tR#m~hfhUK#A%gdH?moIl)|DI7#KEg@y~y#pvK3*cu3&JA|?i@
Tw*6l=9!dYr1e9Z7iHrgOrLz?a

delta 95
zcmV-l0HFWq5Qq_w905nM9T^BxF2VSC)+^3~<|Ln|0|>sJwZFtn^a+0K2T*Sr-a0&}
zw!5CgwR%=C1McD#bp=%s006PHPjBHMCJq1r;}F=Q0sx6nPdKr}XZr#G00004Sz4sJ
BCHw#Y

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
GIT binary patch
delta 1929
zcmV;42X^@I5!4Zo8Uv9Ck+B_10e>!8hxSl_dJNAcpgk!UoIu<#hRBXlPv>NaGj*8k
zAWj8vj<BUXXoQ*jifc(q^pk&_+$lNpznFqp<E&^#bpW}5B3lC|B&e@s1A^PYl&r$m
z?Mu0L!3b8(Ws#)6S|N6+Pc3Kz1EU4vNbw@3D5Q`Y6gUFILl*r43C~swLw|nC$%yG5
z%uGb}<4PvpbHhOLO<EQwr<-|7Wp&W-PKH94U|obgpKdfx=<7foZld)C^&O<ii;*xt
zy7%mDb4y7Yt%ab)7GSKy6eR_q=o7*Is)SOU#6n5&vwpWzy%B3@6wr!zh&IoVxMPxZ
zqXbPg*ZI3W6;C9I*%oMaR)0@y?O#{0gDO8DTA7TEBO(4fuvbXf_vAJ=85E2vr6d;0
z^uQ9P*fJ7gB%3&pE!A46s*olv2I4HZY%EMg6;Gw~)0}h+oZ~K!C+N!T(*G`G>$T1%
zVv3t3G)Y`cF-eY+|ELe1ZRAwpg%~d7=$5LQ1ITpwoW-1osRi|DU4P#9Yhf0%sq&93
z%0kRe36Uu^)Y+%X;RQgb0tU;4HO;bj-(wRGk)pWh1Hv+0X*OONZ~1;UX6H2@?6&>t
zg2z?+Bzce^DbjyObx)nAZCt-lxqDV}Ag2P&OFE3QofzfuQ^@A#jW+#l?6F`=(MVH7
z`5nCg)P3)hZ$aHZg?~*DEF2Ad4Bs|U$!cep7$i)Dv-_$&u+Nl#A0NM|*RB2!n2=$q
zA3foX|I36zD00_)F2`EsWb9~*23b7<p?5;?;H?->z3Y;~)63a2J>hO~BS~_R;Qqqb
zO1*|bHETU<b9WEJI=VPF!lgF%M(ycDqglCz;aHr&s)OYJx_>chm&U>wvF1|hN;yIi
zJq0L>xRQo;uSz)2-1vpC@ZL9|sU0L)s-NZy$Rfj=s6al(E}QzBI-W~_B(}Ud5O0$i
z{q4ouGMA(S&M_)}J|)XRJ<uAxGlahZ!52*DQ)9RrZg5xa<)mbXMF?&vpyoH90AeGg
z-Y_!dx%;aF0DtUJT!9a8sAYXHx@)oIxyK)gL)}F=rJ6f_uq%Yhn_7RxQBpDfm}M|8
zMVH#f=ZIr-(61sZ_E)R~E+}=--JuT=Aa=*o*Crp&huKc>?i(Ct#6ojHPzq~?mhWZY
zvx$8#?KJ~OX19~C3xzQIdXRnX(zf3*w_-Q_3CK5jI)7lTt$B<MVyV=oiyWa=xMRp`
zxPogz*)tW&H$HR#NF@y%wLOG;Dm#4aW^>Ewg?Ir)Da{Y*tD~5R{4Wfl!hRntlO1m3
z`BXwT9!qDS!~N5F3}e8lg7wcopF0KN<r}SskDoOPVxbs<2>zP+;uNB+9JKqig!om@
z(QKE?sDEDU(KavY7*;PSPT^qDt$<Nm;)eHK$vNrir^pFS7G4#`ls5UBpP|1z?!VK^
zMKJ~9nJIG7f`}}n%c2fokI1jVi4UgZyo|{|s#(K?H4#tn!-=HZ$mAWctsn@>=8?N!
z=k1?8U9T{W+C%OIs^#$RfkP8h>=C%^^1e@;Pk$pGMdXX<7vRDSmQ_)7Z!|#$rS+~W
zupn@GHqqLPxjHNwhTbGcb%8>%q`eP=heHzH<AGx762!-$I7j5%3ar-Cj$@^tH!r^P
zN3wtQp46^(m(Xq@aj_Lj%Ua=u;I(vZPH3EW!0Y<zV-P;bA0lW_ehh-fvF21pJhA;b
zIDeYf!3i}wrN=T!jzEl1Xv?%tV?+ioisOh`6)5E~dNMFG<e9eKSyrWZk`V?kuwXW-
zdT2r*Ynd$SxwRFyY&tI8xmPj@a9be_J3;8@G)_|h!;S7`XR}#-4%8Lh6jJ4o>is4G
zE<H|U8~P;^OAm1FMLJ9y9bgIa^O90PbAJi?)?rdW+JE7~^GuXEFy;NxFdF6DnS};T
zbB3tKlZLqpf$H9e><}{bzIvANTV<YP62y$a+MpS9tZPlscqa99mz@Vcu32YpZ2X|u
zIp+A=$=>&Ql-}VpXg|{&f1K-~bO#ug&klX5za79sULW+3z?pdx*wRBwFD9*iNq<|!
zk%$ZDe`ef9vkN{!Em~%D2qsfa+#@iJb>-`_25+KSQUU@x2azv$t$Oi#TA-B$P3MGP
zg51bxYK*U)^l7fp;5(Y`53L<r8)$Nr7df3?-*h?Zk-Uq@N9}|rT4(zzG1E*Wk2TNx
zii(Eu@r-NzOZa2intj{!U}7MG0e>(Nb-~2Iz15;h;Vt2gRyIkqcLKA9{b^+CQ3dV2
zrR{f=-8INq7Y9fo`|flez))#uvLw;v*`G&$jyE~71;G%}Blmcg4hl}?dj{#d!O{G!
z8q^yH2xGY!lOdh0koO5FAw~oX>G?sfp)J^MY6Y!#7XF_|=*$Le`9|%#UV2ROltF+Y
z&p40Yhk|k_8$O<>Bq=4C<m6LgWx*Z+mU_YdM^IU0ps+A?PK&jtCG~jj?!qD*XfwFp
zSdnpZ8R{m=2qtkV+pO!m8j?_2H|j?#<W_h900000Bs6y{=RHp-00FHLlIa2fUC0}_
PvBYQl0ssI200dcDWi+hK

delta 1958
zcmV;X2U+;k5%3X^8Uuz1udy9V0e?jej4p~yl5T3<QHayyFm9S{jV6n#2Ja7u@QaIV
z0wA}6cm>wHP6H;y^a>@9er3`mxGS1?lg69~&uCD1O5FXx%fjqb{#kTm?Hz+sMv_f*
z)o7=MI2BLM3!g&!TVwJKM<6}--+5pbRxVQXZq*=_{uX_$pd-m=6G<VPf`9M$%>8AI
zUWNz$SO5rWcqCS_fO;>%H^N9(Z#_oJRV6dV|EpnA!|eoTNZdt6kWz=!;KgZ;7kgc)
znT{#g3)S^$0{n>3OhxM7JXD!*_ud9k7I~K?lC7-EXpfhcqA-Fv9RW@ICj1h?H_}D=
z8Su(eWU~GblPiOrc7-_J9)B4Q_$x!hbXI>!h)TbbGV)a$5f!b4z<A0P_{agCM3YLF
zCuXiyLFy~N`y~Dq@RI@88)UmKs*fQKYA{6E8co8Jj2c@qClMQ_Iu}UXj$?fD?$hKd
zS%u_Buq?Y_#gWeV%D((OV>SuP^u(pLdBa9QSErD|s46HXrei7^3V%+%pGjW*Qa$s5
z@~C@brTBy>^f$a-H2oPLrM^K-`p(L!5wH9ma9Na)h;Cmm+GkrzMO^;`sQ~}uWk`DK
zAK=qsi1H4{1-It!tL`L7xO9Lc|Ei*iiK@&zt05C@fBi5hZB|h2(P;B*_XtkFal4@M
z<D?r|6WjY{ZhmRYdw(I0CbK6k{E+LKig|}!Wky8ZRt5LN^^XH$LR^D~;nshu>J>BC
z2i)Ac>Hx}FmW3}KyKZ+#hA5vPDiwVTSlVF6%(8c<m0Lp?&4y9cs_t1CxAtb8f4mV+
zG<|Lyknrawg*Ez@r*#SAp8az3@BZ6M-<HH`B8<PA(SFS5)PJuQX3jcm<*ZLrte-<i
zR3oNX=yeVs?yWt#6C3v-0B%1i<Mvo=3k-9tK2K*0;`uW>LdjnTsW!XtHV+fh7e#Aw
z>YvW;<-GkQka_~U#!6Z0X>%{OQ!c2|F#-Ohvt-$ErjDZN8F?pw#K`z&SkMKV79-Ki
zzxK{|%t@|@_kR+4ZueIu5XN~>Jn!?OK3GavxL{@e8$!$mcNHPodhWIQn+Xxcfc{W|
zf{4D-fKFw6sRv1eU-{_q3jhumX_fq_wV{w9>RD2%tuqGqeARZx$K?^uSW*Bb1#nq!
z{#K4D>%e%fK0_Ig5a=J*>cmSKp(iUNZ5kA-I<}&<9DjeaDLfoFVNrAsq$D|{fMvG<
zsv686o00|qbZ9CJl67Mw1!y@pT&;m(D!OBA^b626DKz2J-fI|#W&1`*bp|FC1hU#G
z4Zed`r8YRtJH;fBbSQ5qZq>|5lxP?jw`S<0SQ|n#&c=%@Jd*?(sGfo{pEOEzd?X&7
z(h92&0e=+n52>`bZZBivZS#HIc7imITV5>MrA1vkfxFSTI^j^?D_%kIl4Bp9Mm9Q-
z;&mC7IzIOQ8xj;A*Gr<EF{`xZvQyAtzdl=Udif4l@*)1bDO%8#-~^hxT{|(r3z`?7
z`BkBxhHMnM=IF6oAFI!?*B#rpr*&U%)dPsnPJdY|y}kRJ9<rjNf(y)h7LIU;^^){*
zvIONSr<?0_EmS3DH~H9Dxf)<?L)&L<->-NYQ+BOb<3XF66EtCnUb_HLVFim2%kKQ&
z=<IU@-Mh^wVZW;ID(r@S1C$ZOrEn{#i<%6}3ISM!W#de}XfAMg+fdv3`@aSv8Ky`b
zwSQ(IHMU&_{V(?oF?-6?43C_~`qdjOn}Z7U7&JwOO#pX<wNHbaJ9}Df24-^x1Z@c0
zoQH|HQ?(}v^V)$yT^|#>kS0KI2W+Jc`VaC^A?F6ipnv4%%<_C6@pb`z!R?3yyZGe@
z?&YU&<!D+a#W1QzF}(#PdsnMOqB%^=0Dn`{ZSTr3vxQ@{@5U8qjr2+$5g4jpoVk~-
zG~G^D|F86dCo2^Ph068)rXMpavbO++Z%*rGu%y#FfsNlaZ-7YQ-)mq%6CUJ%K^<_s
zqGo)Pi>VTRhev$*kg4<8lg=t&H^m%@eoX;=b|gFHYWX3Yk%x}K#k&F#`z$dB^?&$I
zrU+F%h}s0`f%ou;lcNvhYp-I|`rMmOZAQH6PdQ8pavkcBD(Wv>xaB}HJs!{QhK&vE
zC+GTyku!6X=mCW4z+qtoc8M6&?cmvO{O+4{+TVOO4)h3cm>=4tiotIR1tp28^;VR8
zcvi?cEAFcDh(uz@x{u(^m?y2J+J6e?S*whIH>6_W=nuo>#Aq9`TEDMl^40^?b3P_=
zMse8HIu$wbuW9yYF?gNO$NZXOZN3}Y;i5ezsRqNBBH1y7b-^>^HjhGGdfLb+2+;Nt
z-C`QBuILe%F!l1>E<E9#cu=D+klWDXw8k$a*bB<y8emW*jRGb44!T;}g?|j8CRL6g
zS%v%N&S2P_On>hDE6<(KFd_<^CUe2#h_1t5XCJTGI^p1uixo<V-B^JbY$(h4gAl*e
zY<XbJ%j(~pj#pL_nW|*bM9~MEw3FT#WB;EYRfP@p7cGiXM>bSV`Q+aGR829G>lZkg
su6-{4;!ywqT;+5%Zy<Of02cwv5r^pl0Jnp20kOnq`vL#}000D8T1m#cTL1t6

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
GIT binary patch
delta 58
zcmeBRZDE}t!|1$G){05@pIX$Prz#C$znRJz7>qU69^lIE@MK`T&$33IfkAv;)zOVd
N(tk5C00B#66aY$R6HEXA

delta 62
zcmZo+?O>fC!|1kA){4pS&jZES=!od1b6X=89K6oJz+kMg_5fFQhbIH$BbGJt3=An<
S^J+I9N&n3Rlw)9ti~<0`Jr$b(

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
GIT binary patch
delta 69
zcmV-L0J{H_3V;fb909<w9jgR5J)&a$oT|37Au&J6Z`m)ToU{+lq#*zRam`p{fdq<F
b00G<y{cQjM@%*}<vBYQl0ssI200dcD_9Gl3

delta 89
zcmV-f0H*(d3X}?v90Am^9jgRP9b;j=`r_vYc2tbi5M5qSY?xLqk8jc>zJoW;Z>Z?W
vc{zzqdAVZr)Exi-am`p{fdq<F00Hm`{cQjMygAhGvBYQl0ssI200dcD*N7#w

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
GIT binary patch
delta 70
zcmeC+{K7FohS7MVtQ?EwTrM^v=h}r*+_(Ox6wWiS?_py%<~S9>z@Wcsg{|J_eYFgX
a=Q+0dF)(~=Y75+WB>guN0}!x8MgaghZ5Mq2

delta 90
zcmV-g0Hy!*2#5)g905nM9UcTtoZzp4ZEY+L@Gr!!2}ZuBx4?KMJ<sG>&~YCkt><P{
wo3f_Z>WZ%Pr7j2n057VjJudUUeE<RD2)0fD0K7-&A+f|~`vL#}000D8S`&aKQ~&?~

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
GIT binary patch
delta 74
zcmZqRdc!$EhH>Ra*-0$6&jhnx1#-@nH5Lz;wngk5+xv^W|DB%thBAPFqy8F)<#)L!
bGcX?IeBQvw@H*?6&Bi0?znMUiERj(F6MY)>

delta 94
zcmV-k0HOcv34jWa909<w9g+l5<-Q4F+rGxV`BohBw6~pZv~iC9gkI7j$$p%DztoA`
z{bm;NZJU@)!Yl6!<P#kR06{OTK&RaclK=tS3Fm+T0Ju3n7_r1>`vL#}000D8TCI;N
AdH?_b

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
GIT binary patch
delta 58
zcmX@XafD-n3?uVK*<Z}M>GyP{3@4jb9ruc2U|?|D*_fLA%8r3?KF9wE28Lp%{fjpq
ON&n3Rlwx3si~;~wqZ7pd

delta 62
zcmX@Yae`xl3?s)z*<Z|t{snLNr)YO>m()Bek!K>!z`)?PvoSUKl^p})5{~~73=Fbc
Sna*xJlKz_sD8;}M83h2M3lxX|

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
GIT binary patch
delta 85
zcmeyseuaI46f+a^#Er6r%x)9n4k|I23w}H(bgHhR;HvluA?CFYdUH#+IPP`&u}@8k
no0kCy)E|BnG>x~?XJA~*-t57^5O97{=*A=IznMUiERj(FKu;Zy

delta 113
zcmV-%0FM9E2k-}w8UvsMuCX0)17b>Vu0_2l7}KNxx=1Bu%vAALsDWQgR}`FqpDe1L
zqV2tOM;c;!jpC@*p&GxEm&EC6C)9J?$+b!o7rvu~00000#W6Un^^?HO00GJep-BJ$
TF#VcKvBYQl0ssI200dcDK*cc%

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
GIT binary patch
delta 64
zcmeyuc86_(45Q3OSsrHNG?6{rbKmVxQ4MDP{rzEW$$JKd-zyw+@Bdkp#K5?NZL<{v
UL%8AgIUA3p|7KzU0+z@q07dQ?*#H0l

delta 88
zcmV-e0H^=l2J{Ay904-19Sj3YFy_jao>g4}2EA)35ptCUhUKdeT<Q8>@1$At<2nr>
uUX5*uI+8BX0002{s6Z{>{Gwt20nP@qIsgER-^@X=#Ao{g000001X)^2$0Kn7

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
GIT binary patch
delta 60
zcmeBS?_i%G!|1wE)`nR>Ht%HSl;pQ>Qd${6;NhbU;m&a@Js21tvQ4mJVAzqdk#*yd
M^xsS%NtVbc0E9vmdjJ3c

delta 64
zcmeBR?_r-H!|1tD)`r=b@qAoR{jIg4b|q7~UK|W$0D^~)HiSFJt@L1Ee9AV#ih*IB
RmcqP^N78>Yfh1WXqX6FM74`rC

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
GIT binary patch
delta 61
zcmaFE{(^mi4CB&`va^{DK6pLYGDl-}PN&AaD-1wz_2$X7x2ooaFfblu-($<bVC!`4
P!p0-%znMUiERj(FEH@Z#

delta 65
zcmaFC{)T;m4CAVeva^{@t_bg0&0il|RLykKuyarKHU=QLdh_JkTUGNy7#NSS@3CcI
TXf3*YcH@!s-%KD$mdGdoc$gW=

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
GIT binary patch
delta 2908
zcmV-i3#0V>4!9VQ7zN=iqYL<v9p!%-5J3mil(E}GE}6n$b>|wX1UnNVvB;Osio2^=
ztCge(wby*|Z?4v|B`Ci6k148>^xC=%FKb(V(-GA#SD2P9azO=vs8Zc2(1Pka;-ce;
zi!^-Slp`NGtn+9d6K09DPMy%kd_`#NE%>a31KQmYy`(K6pb^2ee!9<;Jjs8h3A8j2
z1i|{KNE}9e9%Yuh<nMBmRDBg*M)RlKAal|*x6eCn2<vzJjoAO6kV|{@a;k9<FEZv}
zw!@*W=gXWg<8r)NT;;0hb0{e6fm~V*9hb?phC2X<@W#RAaI~m0QV40Y7z|1+kv<|F
zL7Lii<v+<I;1~Yn2rR82UJQSr&=c%ovvex9WYm)<p@q1@6*pc(Vjv!<km{T^jiZBf
zpS9C*P;w=q!30L;N4hHSaznZDXd`pUj-E((y`zPaz=4#*&+f?IcV-6c8TcZ26(@*N
zE8!hxh>PsHq8eibuRW77C}L7Na{)X_#R|*6t~j;BYgy#}>9hdrgam)<9Z#idL&g{!
zlWdA^&N)&I3dQ07Me5pdyE7rL3kx_fSt`>+n+DGDC*?b$0J=(}Rc!1kT$3tog<2GF
zYa-p^K4<$!0b~=1x^%^Sl?zZwx&beycbx8<7HjISZ%TZbh+r9~g5#y*0kM`p>#iAO
z53=Voiir*XVbY%8a!`LSJTq%EUK1M{OI1jdMN(~k5me*{igDvZZ2o%Tyltx<gA@LB
z8)n)@_&@X6kImeH;5&%D@r#K5w&^{SZpwC}?85IpTq_~axaAZ{wPlDt5Xy~G-d}+s
zV>#A8My_@Kn%P7Qbe)wNYiwr`>np=J^{;z2P={FA9{iL7WF3F<0l7=tE<pfV&V;=m
z5yqkrR1&lHhpml*uud+6^|B1rexi=FKi$FT?3@N(HxddlP2SV~U`+Q%Fsg_^Tvqwz
zn6PX3eL{0s4ZuJ{tIORaf~w23zxW9+6FTr(Z)P1FF138Z+I01)lZ;rK{}jjkt(dBk
zyH5u)Ht2rZG~<6H+=Q~C6)m$>r_*|kc{2Z&->W*661sdsGw!|MBgaUhEDaTYLLs$J
zMe1i>#(}rDdghDaa39a)scrh5T)z|^a&E)<VO~PO$I9ZZ1#E!}%$<=oM%w}^-06{z
zyMmm%@~-zIC7A;x2FS{fzGGV)gG?mJr*E6&*~M4Ci*<iF@j;p7GO_B*&DkEfAXW}}
zp2Q1M&wOWE2N104nfGHFaLVUj8RvRgy{COBz!YNsFv7b!cX)ll$&*V+Mo9g_q1(Z{
z+FsDk=nQH@o!(GiI<ZhN-OmiRGf@D!!>=LWM<r<7GXE~EUuk~wstev(I;n0x%xjsm
z2MT6It`&a_TS)FG=h#0(nQ^5II$Xl{<<52PR*lOY58H{OhDlMJH=6Y$M;3CE**LBH
z#;y$)7v3p$<?Eej5LlNkn$9Nv94TQm@qn_B>8eM@bB(z8?)8jy^oWM!r)FiLjpJ&g
ze0F2$*BIY<4Up%OzZ72Ll#;RK`_wK7+F%j!Ffo5TjaYhqlCa>n1CWhZ%C}sOKqNRH
z>xpu&QT^P|dyzlBO0DlWC4%&R0xVK2O@3)7ehxBj$C~hHN(6hv_|(&*)>MP#gT<Z`
zRHy21xP!Ngr<MnK#ZuG!0W6jU+2^~1mf*U6uM^`VfnbM8o|N+gBM;|8cweSB`1hoD
zB1L~EW>lFOtcKimHa4wvuEQvq9vwK^exsg>bzq-R4IeOeciy3v8Mr|yetmiZvjH=i
zFs2?J*$a;>I_o1<Tvq=QaM?XE-uZ2z0TJM+N=bAQdX*;h|4M<DTKMRI)%k|Uk*47B
zb!Q3@PWk&*lLYQvJ?(|&+%JZ30U!~E)AN4-dM<ASjh?{6+$U7)uWdf$3Y_T}J2y43
z>$7$$GEo1WD#&*O4$<4$`WW)<;Eban&`qi7wswnP*Fk?UYw^50VQ8My5vO|4%1S`=
zK6BWWg5>v(q@`mMZLF#kxaLvyMmkH*aqJkPBa&FzIla}m@>LwN3E`9C`1v|u@<M;)
zk?YE@RSCve!BR<j*};5u4EeqIZBKb*@XEwWhDQ&<s$_zAfLdG%KqT3N?7h6U>TEWQ
zaDsXWd^AM%KLfml<L1*iXqQPa#4HT@Uo0=PBteazqEhf8Lwl0A+SM;T<;i863`YgS
zYw*k%AuWp~CdfdkEcb-+cEFk`nJ<6#oxY4)&X_a=UQg6IRRT<tR$>zK<BRzz8vA&m
zDZG?(gqz=|c>34u2c)$3R<gD`5$4?j{BQr_-Fg5<$UDTqmQAof$Y4_|TKKv)>U;D&
z`P)?W3L%M?y{a_JfAK;RWSSB5i0$;R2-LSM^(${F(3oQqWn3cew`>IYtYCjQ?}6T>
z=}zKSst4T2;$_h?5bV*I0|OzYb2NCQ)Go)gA_v0~$W}|*F!F763@fPV74773&99d+
zKgn7avw1m(wEgvS$Rk|fwrix^fjfDuZmJs24)SR7@q-!nd^xiT3uv)5t&&P(Tie4(
z7ebWOpl@)4q1QN8kOv)-fD?b}a?2Dm<gLOc3!0u4({DkY%Y#Y|s7|TWq0IV`T`1r@
z@fx|0Z}ylC6^<l+Sg{|mFWV(cHjg7)dgdd)Z^t2of<h6s__V@`L+(f~?8f9^|J|_Y
zTi<l^9pe1+Kov(PG;<V1Wo~*HAe@upauDAwRuOjAUP*qnIJ2iEjAeh(#7q-&;uN75
zWT+%5+8@tVHJh32lPQy2V|A4vQG#_ca?=0p61K5Hqq^j&PA)ICXx)oD-9K*@w+Kg=
zrI_-X+MF%u1eW4ZvUFPctg853xn#PFZ(o>2I2&hli*HXwR0;(`4upptihH1rZ#o%5
z5TPZdyc^)ghV#C-7-xSCDHzMzKdlbb6P04c5!XLX7u;LdUkDuIL3@$+6|gj~FIMeD
zl}IAe#iR9hMaTx<nY`C)WZ+9#G)nKQpqvu$64gK@I8BZ{tPL5LdJGT3hGWAw&@nML
zh<a=25<QwQ!==?k(O8el!h3<4on^4^{LgM4FiLOpWv<CboUwmZbJ+}03Q&ErstNEs
zT;qL)_o@*KbG@LDb;+x-!-1W9r(;JJUSM&pD@MX>O9BW2f-f~!x%DGd<B@i5=QbEa
z0vYM*T6;K5=wWIMjy9ZLnl+9#Y@C?=TDCZxp>4174EuyUFyZ=w|4UtEIO&fr6?n{L
zWv7kLI;ZGW91DLqhpnq99032m?h^yDS+R#CN4FLf&WbV}0_AQFZSg`AvZu)V%|=E7
zcQ&sP8(Zyi;Lo<X34=Zo-LHVL1X7<d41FYZmbry?tEJMgtYro~LeXP%5Yyw{Jp*YZ
z8{GmAToWd=6wb<pH<bYy29(vI{ES11O63;Wa$TL9VorZt_S*IfvldO}coW~>kTygQ
zw7BfSH|O4dLK@&XgX}4HRyZAAFx<7y;~VxJef1!_u++01nZ)P61YU_}e}5Aa$zFs<
z)E>&3*$McpCo*f28Jj2!XfFq12Jdv2JC)x%@NM5Cxr=1>zUpA#l(|R44ko%;Kgua0
zv<0|bm;!$k|8yq=Gp*VOwCDzq>{nCHxq8{}oh{XTUIBnEU0SyIpVy>@OsGeors30%
zDTg1?|4JN-M*#zNEsj9FL=ZuLKNY(0Rw=CRFXOe=)bUU;2}2o>g1cTeYb{F}r}c+f
z7sn-A=R@#cKhW`0#o!Yd%bK(-(e*@QT#yxwXopN0Js?cQjTY!qjvg1(#}|{6g6TK7
zl{4{?qK%N(W!SuqdfXgF%0b1P7XScx^u0<6RnEo$0hAb|+XMhi&5JUz#Ao{g00000
G1X)@$0G$K?

delta 1687
zcmV;I259-X82k>97zN;k&Ide^9p!%+|C>Tb+lR{wPQA=o=bEXZ@&-9el<W$H-c6a6
z=6Kw?=k;Ahy??YwYXAvv+KYbOG8|#w@UNJz%AhaT=YNHlaaSykRLJHK>I)T#ngK%I
z-ED}@-7}g9&&6TRdv!qf#Y+u74|Ofq+xBIA(AI-;sDvzb1b;5IOS{$I$J>7w_R+2Z
zM+3H1AmjKo`kZeU!nUTjYC&DM-s`h9wRKYA@?n49GQd}zYCIRHFIk(p3En+ta!x*p
zuG6cyFzVnIw%DF%b4@kNC~4}E2F7y!9{7;FqJcq@4YHJ;7}4oav0%~WTyo860vdLD
zVHd~06^=c#u=a&&Y$t}iMAm=YI%bGde#a}P^6~eZr_b}1m}1c7kku2fMxcB($tB%z
zw~pI%&bO$G?N;SKnmW>X4FMlKkb*MPUa7Qi#$r(tTe-G2V{s3%BN_CbEd_qiMP38I
z<Mt@*Z+2_T?z8!^i~RQiBI|S_E*z6VImB@2fM2gmi^>65Ds9BH+f#p{W~cl^TnY|p
zhPuwDE2wi(+ef#>SHU%r>f}a3@#<i>d|ROa|FCud+=KdY_8mLB$1l$!?s(?+0Sg?4
zT&;rstn!Jsj<cKEO^%B|zijF_=+Y*4Y2@ihTkMUxOZ&Clu6Vb8i`p<zWvHCGk84WJ
zR2%O%_L}MwO5YiP=+b{XW7%BiJ0-J@m@d2~k7y5ZPR^(582wE|ym6q#W!g%V5n96v
z-;*w?yH%6P=jIBnS9`263W;rOklaR^+nARbgnZnISI5E3PNk_KPBq8AyDezjC&dZc
z2T$Bc2ZfT7M~PqSo&KW1@#RRJ9DF7-a7Uly?`#8yU?Vv;R;hn>D&b?qPN<dg%wKIA
zY<?|Wgtn#&Te{IAyB9|;TnIh_4Z0PmA~naw78F)|8#eY|e2vM9u%gN^weDQKg;q63
z1hX|-{Vy|rECh;n*NuH+F-tcJKz<5f^n$JdXEu2rB<e)x+_Jhv)mLxY4sD9LH%oUt
zx&~Ty+_lUKaW8+T8~8QG&nY_l?TLmSkr`f49`gGpoRi19<$THJ{M!QEFd_k526wej
zhkB_LN;2U~I6Hu!4;18<VYvrYKMmK4h$u%W*o2D2xQ*Zo(f8DArCx)^fiOTY`0Bf)
zi_MPcR_*Qz6br42skHrC^@CVU&o|sClDTh@v)*8_l&ODk{KnBJ?et3RIJpchh&tk<
z?4;gPv2mR_<FZmOcm=#(sn`X`6?{FG_gv!RFDWFaq_wcE5#5~S7^>&l;3&P01qy*`
z%oBNC?W%r0mF2v&tWB!=0ur!?Em?CGpkWG6zjq26$gj|37i@ipm?aQ_F%8C}JHw_%
zNIqWII+lM@ir6<XKud3Y*7K861yyBE78*7K&w)?OOQ}-2?Y6g)+_Rzc6|Z21eANxs
zaQs<&zq#Tj+_=S~sRI3wHp)RdOamR`wvu@^L;dnJGv5A6{15v`fi{Q(h*5~3zXivF
zV`M=Mq?otE-wjKy^rh$+&YhJ+b)lvo`RI+Z`!Ij;O4`8WQAb5y{Fq*pKQ<ZtQ_uoz
zn_Vv0@k1C~5z*k1akAY(Lt?0;OtkVwU2!4hAyC4an~$t${ERZGkN9+p+y55TCj0sh
zHq#BU$n@KjBEbm>82M=wx<S-ka~+{E;=^z5P#wP?E>2=3mjU<EaKI$zYTi|R{h9)-
zCCPs!jd3R)1G6nBz&|h-8=rgBPt}Inyk_()O8)8<!~75n0#g)G0b-XtHd0-{80LPq
zrjB38U;Rv`OQ?|y&TfdHlrE_O?%kl8L3sBW<`U>|=>3nGqv7wy>KM_q!uv~Vss$^K
znT%>+gpW~ucf#cna4_8AbhrrUso%r;Q$~M+76Bz)`8_7CDYuZXh%C+;#pf-oLpbbO
zH*GYT#|(IjGRqe?2$WYABtxpnm!E=NxMNy+^{s0~NlLq~vIpSi;)M+fD}oK8)efGK
z`%{j*5vPb2&P*hnK+FY7>1VpkTs@5Zf+GJrU1}PL0auX@iL}EANL!|11)30-t|osE
zhs`L%#DO_+fZl3M{1l)W^m<iB_ec-K%{Pixt$r2)rj&D2tGO*1ye5!mLf@cV<8FJr
zE$05w;umbx9wE&nO~o^)IDa45tWuz?|7gy#h%G%QCRDHJ&Q-->VLp+}eC5>u029TA
h_h@jtp8x^a4$q4M08N~5bFsu{`vM0500004Sz4C;PAdQa

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
GIT binary patch
delta 57
zcmZ3&IfrwC3}f_0*<co(|LOman@#0j!DPX}5NP1FhfBKa5(DFRj<2B%48?nD6*eA8
M|INez1T2wJ07JPGJ^%m!

delta 65
zcmbQkxrB3q3}fO(*<covkH>ePTJ3pkmwNc&1{s!P9~pok(7<aCmvq-92FAY}Uqcxf
TMCU(i+;}AYHxo#bB{B*CL~j@d

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
GIT binary patch
delta 70
zcmV-M0J;Bw6yy_-908=U9gYb(VaZNP%g%)CQ-{KmzZA=tmCWLrYFmiS0P3yco=2)F
c0005N6UpQP07;x>VzI<$`vL#}000D8T8Fb9kN^Mx

delta 98
zcmaDN+#oVRhH>vk**?xt-9?kFRx3om+VuHEDnFx;S%KTk9tP$3;)&YlyKU;#=ADkR
zi){#D^U1z<#@IboxRU_{UafsJ&wZ690|Vnt;ge687^Kecaocz#{WlXxk|i<<0A!sc
AsQ>@~

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
GIT binary patch
delta 74
zcmZ3(HHT}04CBp>vWHk~?OVUxU2@FZ<=&*pP4$xh-}JRAo9#A#u}zBs2wrMDKL2i$
durveXSI)nEj11eqFXP>KB>guNNRlNo3IOHMAAJA-

delta 90
zcmV-g0Hyz&3ako{90BXG9l``nJKxGrz?`Au&#+vU`<$tK{o{;Jw<r^^)c3r;*MY@S
wisgEtvthN|(+m;-0O=^>&+f7l8vp@^3jK}&0IebH46(##`vL#}000D8T3fa&OaK4?

diff --git a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
index e69de29..a003a31 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 7a1dca4..7fdf80f 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 774145b..5c9ef7d 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 1b100fc..ed045fe 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 7a6448a..ae65cec 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 bb10aba..a75d096 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 aa05b40..b5fb88e 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 5953225..5d4c2a6 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 a9965ba..f9fa1b0 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 ce0b425..50d9572 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 f666431..7ad9610 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 ebadc26..e6e3184 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 ❙
-- 
GitLab