update

build.msl

+log console
+log html build.html
+log+ archive
+log+ mmt-omdoc
+
+mathpath archive ../../MMT/urtheories
+mathpath archive ../../MMT/LFX
+mathpath archive .
+
+build MitM/Foundation scala-bin
+clear
+build MitM/Foundation mmt-omdoc math.mmt
+build MitM/Foundation mmt-omdoc units/dimensions.mmt
+build MitM/Foundation mmt-omdoc units/quantityExpressions.mmt
+build MitM/Foundation mmt-omdoc units/units.mmt
+build MitM/Foundation mmt-omdoc sets/zf.mmt
+build MitM/Foundation mmt-omdoc sets/nbg.mmt
+build MitM/Foundation mmt-omdoc sets/typeconversions.mmt
+build MitM/Foundation mmt-omdoc sets/typedSets.mmt

source/sets/typeconversions.mmt

@@ -25,6 +25,7 @@ theory LiftSeparation : fnd:?Logic =
     include ?SetTypeConversions ❙
     include ?Separation ❙
     include ☞fnd:?Subtyping ❙
+	include ☞fnd:?InformalProofs ❙
 
     axiom_sepIsPredSub : {s,P : set ⟶ prop} ⊦ elem ⟪ s | P ⟫ ≐ ⟨ x : (elem s) | ⊦ P (asElem x) ⟩ ❘ role Simplify ❙
     axiom_predSubIsSep : {t,P : t ⟶ prop} ⊦ asSet ⟨ x : t | ⊦ P x ⟩ ≐ ⟪ asSet t | ([x] P (asTerm (asSet t) x)) ⟫ ❘ role Simplify ❙
@@ -32,7 +33,7 @@ theory LiftSeparation : fnd:?Logic =
 
 theory LiftProduct : fnd:?Logic =
     include ?CartesianProduct ❙
-    include ?KuratowskiPairs ❙
+    //include ?KuratowskiPairs ❙
     include ?SetTypeConversions ❙
     include ☞fnd:?ProductTypes ❙
 

source/sets/typedSets.mmt

@@ -8,6 +8,7 @@ theory TypedSets : fnd:?Logic =
   include ?Powerset ❙
   include ?Separation ❙
   include ☞fnd:?Subtyping ❙
+  include ☞fnd:?InformalProofs ❙
   /T the type operator of sets along with its constructors ❙
   setOf: type ⟶ type ❘ = [A] ⟨ x : set | ⊦ x ∈ (℘ (asSet A)) ⟩ ❙
   fromPred : {A : type} (A ⟶ prop) ⟶ setOf A ❘ = [A,P] ⟪ ℘ (asSet A) | ([x] P (asTerm (asSet A) x)) ⟫ ❘ # asSet 2 ❙

source/sets/zf.mmt

@@ -112,7 +112,7 @@ theory Relations : fnd:?Logic =
 
 theory Functions : fnd:?Logic =
 	include ?Relations ❙
-	include ☞fnd:?InformalProofs ❙
+	//include ☞fnd:?InformalProofs ❙
 	
 	prop_function = [f,A,B] prop_relation f A B ∧ ∀[x] x ∈ A ⇒ ∃[y] y ∈ B ∧ (pair x y) ∈ f ❙ 
 	// TODO ❙

source/units/units.mmt

@@ -24,7 +24,7 @@ theory UnitsExtended : ?DimensionsExtended =
 	m3 : unit Volume ❘ = m² *'' Meter ❘ # m³ ❙
 	
 	mps : unit Velocity ❘ = Meter /'' Second ❙
-	mpss : unit Acceleration ❘ = Meter /'' (Second *'' Second) ❙
+	mpss : unit Acceleration ❘ // = Meter /'' (Second *'' Second) ❙
 	
 	newton : unit Force ❘ = kg *'' mpss ❘ # N ❙
 	pascal : unit Pressure ❘ = N /'' m² ❘ # Pa ❙