Moved types to MetaTheories

source/DefaultSituationSpace.mmt

@@ -30,9 +30,5 @@ theory DefaultSituationSpace =
         include ?TriangleScroll ❙
         include ?SimpleCircleScroll ❙
         include ?SphereScroll ❙
-        
-
-
-
     ❚
 ❚

source/MetaTheories.mmt

@@ -318,6 +318,44 @@ theory FrameITCylinder =
 
  ❚
 
+theory CircleType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  circleType : type ❘ # Circle ❙
+  circleCons : point ⟶ point ⟶ point  ⟶ Circle  ❘ # CircleCons 1 2 3 ❙
+❚
+
+theory SphereType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  sphereType : type ❘ # Sphere ❙
+  sphereCons : point ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
+  
+❚
+
+theory RectangleType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+
+  rectangleType : type ❘ # Rectangle ❙
+  rectangleCons : point ⟶ point ⟶ point  ⟶ Rectangle  ❘ # RectangleCons 1 2 3 ❙
+❚
+
+theory CuboidType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+  include ?RectangleType ❙
+
+  cuboidType : type ❘ # Cuboid ❙
+  cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
+❚
+
 theory FrameITTheories =
   include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
   include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
@@ -326,32 +364,25 @@ theory FrameITTheories =
   include ?FrameITCircle ❙
   include ?FrameITCone ❙
   include ?FrameITCylinder ❙
+  include ?CircleType ❙
+  include ?SphereType ❙
+  include ?RectangleType ❙
+  include ?CuboidType ❙
 
-      makeCircleOf3EdgePoints : point ⟶ point ⟶ point ⟶ circle  ❘ = [p1,p2,p3 ] mkCirc3D (  Ppara p1 (p2 p-p p1) ( p3 p-p p1) ) ( midTriangle3D ( Δ p1 p2 p3 ) ) ( d- ( midTriangle3D ( Δ p1 p2 p3 ) ) p1 )   ❘ # mkCirc3P3D 1 2 3 ❙
-
-   ❚
+  makeCircleOf3EdgePoints : point ⟶ point ⟶ point ⟶ circle  ❘ = [p1,p2,p3 ] mkCirc3D (  Ppara p1 (p2 p-p p1) ( p3 p-p p1) ) ( midTriangle3D ( Δ p1 p2 p3 ) ) ( d- ( midTriangle3D ( Δ p1 p2 p3 ) ) p1 )   ❘ # mkCirc3P3D 1 2 3 ❙
+❚
 
 /T The meta theory to use for situation theories, scroll problem, and scroll solution theories ❚
 theory FrameworldMeta =
   include ?MetaAnnotations ❙
   include ?FrameITTheories ❙
-  include ?RectangleType ❙
-  include ?CuboidType ❙
-  include ?CircleType ❙
-  include ?SphereType ❙
-
- // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
 
+  // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
+  // include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
+  // include ☞http://mathhub.info/MitM/Foundation?Strings ❙
 
- // include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ❙
-
-//  include ☞http://mathhub.info/MitM/Foundation?Strings ❙
   include ☞http://mathhub.info/MitM/Foundation?Math ❙
 
-
-//  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-//  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
-
-
-
+  // include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  // include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
 ❚

source/Scrolls/CircleType.mmt

-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ?FrameworldMeta ❚
-
-theory CircleType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
-
-  circleType : type ❘ # Circle ❙
-  circleCons : point ⟶ point ⟶ point  ⟶ Circle  ❘ # CircleCons 1 2 3 ❙
-  
-❚
\ No newline at end of file

source/Scrolls/CuboidType.mmt

-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ur:?LF ❚
-
-theory CuboidType =
-    include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-    include ?FrameITBasics ❙
-    include ?RectangleType ❙
-
-    cuboidType : type ❘ # Cuboid ❙
-    cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
-❚
\ No newline at end of file

source/Scrolls/SphereScroll.mmt

 namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ?FrameworldMeta ❚
 
-theory SphereType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
-
-  sphereType : type ❘ # Sphere ❙
-  sphereCons : point ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
-  
-❚
-
-
 theory SphereScroll =
     meta ?MetaAnnotations?problemTheory  ?SphereScroll/Problem ❙
     meta ?MetaAnnotations?solutionTheory ?SphereScroll/Solution ❙