# HG changeset patch
# User paulson
# Date 827837154 -3600
# Node ID 60ab5844fe814d280a8e12b77c685ab8054aa184
# Parent  5324067d993fcddaf9440d640ca8c0637b7cbe30
Updated comments

diff -r 5324067d993f -r 60ab5844fe81 src/ZF/Nat.ML
--- 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);
diff -r 5324067d993f -r 60ab5844fe81 src/ZF/Ordinal.ML
--- 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));
diff -r 5324067d993f -r 60ab5844fe81 src/ZF/Perm.ML
--- 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)";