--- a/src/ZF/Nat.ML Tue Mar 26 11:42:36 1996 +0100
+++ b/src/ZF/Nat.ML Tue Mar 26 11:45:54 1996 +0100
@@ -74,10 +74,11 @@
by (REPEAT (ares_tac [Ord_0, Ord_succ] 1));
qed "nat_into_Ord";
-(* i: nat ==> 0 le i *)
-val nat_0_le = nat_into_Ord RS Ord_0_le;
+(* i: nat ==> 0 le i; same thing as 0<succ(i) *)
+bind_thm ("nat_0_le", nat_into_Ord RS Ord_0_le);
-val nat_le_refl = nat_into_Ord RS le_refl;
+(* i: nat ==> i le i; same thing as i<succ(i) *)
+bind_thm ("nat_le_refl", nat_into_Ord RS le_refl);
goal Nat.thy "Ord(nat)";
by (rtac OrdI 1);
--- a/src/ZF/Ordinal.ML Tue Mar 26 11:42:36 1996 +0100
+++ b/src/ZF/Ordinal.ML Tue Mar 26 11:45:54 1996 +0100
@@ -436,6 +436,7 @@
by (asm_simp_tac (ZF_ss addsimps [not_lt_iff_le RS iff_sym]) 1);
qed "not_le_iff_lt";
+(*This is identical to 0<succ(i) *)
goal Ordinal.thy "!!i. Ord(i) ==> 0 le i";
by (etac (not_lt_iff_le RS iffD1) 1);
by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));
--- a/src/ZF/Perm.ML Tue Mar 26 11:42:36 1996 +0100
+++ b/src/ZF/Perm.ML Tue Mar 26 11:45:54 1996 +0100
@@ -459,6 +459,9 @@
(** Unions of functions -- cf similar theorems on func.ML **)
+(*For proof of analogous theorem for injections, see
+ AC/Cardinal_aux/Un_lepoll_Un*)
+
goalw Perm.thy [surj_def]
"!!f g. [| f: surj(A,B); g: surj(C,D); A Int C = 0 |] ==> \
\ (f Un g) : surj(A Un C, B Un D)";