# HG changeset patch
# User lcp
# Date 749830889 -3600
# Node ID 3ac1c0c0016eb4aa7b9460f49ce71827f6824587
# Parent  f3d4ff75d9f266e0afed1cf90c3cf1be76f5edb2
ordinal: DEFINITION of < and le to replace : and <= on ordinals!  Many
changes

epsilon,arith: many changes

ordinal/succ_mem_succI/E: deleted; use succ_leI/E
nat/nat_0_in_succ: deleted; use nat_0_le
univ/Vset_rankI: deleted; use VsetI

diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/Arith.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -42,9 +42,14 @@
     (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
 val rec_type = result();
 
-val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
+val nat_le_refl = naturals_are_ordinals RS le_refl;
+
+val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
 
-val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
+val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
+		 nat_le_refl];
+
+val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
 
 
 (** Addition **)
@@ -101,27 +106,24 @@
     (nat_ind_tac "n" prems 1),
     (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
 
-(*The conclusion is equivalent to m#-n <= m *)
 val prems = goal Arith.thy 
-    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (etac succE 3);
+    "[| m:nat;  n:nat |] ==> m #- n le m";
+by (rtac (prems MRS diff_induct) 1);
+by (etac leE 3);
 by (ALLGOALS
     (asm_simp_tac
-     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
-				diff_succ_succ]))));
-val diff_less_succ = result();
+     (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
+				diff_succ_succ, naturals_are_ordinals]))));
+val diff_le_self = result();
 
 (*** Simplification over add, mult, diff ***)
 
 val arith_typechecks = [add_type, mult_type, diff_type];
-val arith_rews = [add_0, add_succ,
-		  mult_0, mult_succ,
-		  diff_0, diff_0_eq_0, diff_succ_succ];
+val arith_simps = [add_0, add_succ,
+		   mult_0, mult_succ,
+		   diff_0, diff_0_eq_0, diff_succ_succ];
 
-val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
+val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
 
 (*** Addition ***)
 
@@ -223,19 +225,15 @@
   [ (nat_ind_tac "m" prems 1),
     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
 
-(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val notless::prems = goal Arith.thy
-    "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
-by (rtac (notless RS rev_mp) 1);
+(*Addition is the inverse of subtraction*)
+goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
+by (forward_tac [lt_nat_in_nat] 1);
+be nat_succI 1;
+by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (ALLGOALS (asm_simp_tac
-	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
-					 naturals_are_ordinals]))));
+by (ALLGOALS (asm_simp_tac arith_ss));
 val add_diff_inverse = result();
 
-
 (*Subtraction is the inverse of addition. *)
 val [mnat,nnat] = goal Arith.thy
     "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
@@ -252,148 +250,129 @@
 
 (*** Remainder ***)
 
-(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
+goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
+by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
 val div_termination = result();
 
-val div_rls =
-    [Ord_transrec_type, apply_type, div_termination, if_type] @ 
-    nat_typechecks;
+val div_rls =	(*for mod and div*)
+    nat_typechecks @
+    [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
+     naturals_are_ordinals, not_lt_iff_le RS iffD1];
+
+val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
+			     not_lt_iff_le RS iffD2];
 
 (*Type checking depends upon termination!*)
-val prems = goalw Arith.thy [mod_def]
-    "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
-by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
+goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
+by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
 val mod_type = result();
 
-val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
-
-val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
+goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
 by (rtac (mod_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val mod_less = result();
 
-val prems = goal Arith.thy
-    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
+goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
+by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
 by (rtac (mod_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val mod_geq = result();
 
 (*** Quotient ***)
 
 (*Type checking depends upon termination!*)
-val prems = goalw Arith.thy [div_def]
-    "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
-by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
+goalw Arith.thy [div_def]
+    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
+by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
 val div_type = result();
 
-val prems = goal Arith.thy
-    "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
+goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
 by (rtac (div_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val div_less = result();
 
-val prems = goal Arith.thy
-    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
+goal Arith.thy
+ "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
+by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
 by (rtac (div_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val div_geq = result();
 
 (*Main Result.*)
-val prems = goal Arith.thy
-    "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
-by (res_inst_tac [("i","m")] complete_induct 1);
-by (resolve_tac prems 1);
-by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
-by (ALLGOALS 
-    (asm_simp_tac
-     (arith_ss addsimps ([mod_type,div_type] @ prems @
-        [mod_less,mod_geq, div_less, div_geq,
-	 add_assoc, add_diff_inverse, div_termination]))));
+goal Arith.thy
+    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
+by (etac complete_induct 1);
+by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
+(*case x<n*)
+by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
+(*case n le x*)
+by (asm_full_simp_tac
+     (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
+			 mod_geq, div_geq, add_assoc,
+			 div_termination RS ltD, add_diff_inverse]) 1);
 val mod_div_equality = result();
 
 
-(**** Additional theorems about "less than" ****)
-
-val [mnat,nnat] = goal Arith.thy
-    "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
-by (rtac (mnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
-by (rtac notI 1);
-by (etac notE 1);
-by (etac (succI1 RS Ord_trans) 1);
-by (rtac (nnat RS naturals_are_ordinals) 1);
-val add_not_less_self = result();
+(**** Additional theorems about "le" ****)
 
-val [mnat,nnat] = goal Arith.thy
-    "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
-by (rtac (mnat RS nat_induct) 1);
-(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
-by (rtac (add_0 RS ssubst) 1);
-by (rtac (add_succ RS ssubst) 2);
-by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
-		      naturals_are_ordinals, nat_succI, add_type] 1));
-val add_less_succ_self = result();
+goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+val add_le_self = result();
 
-goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
-by (rtac (add_less_succ_self RS member_succD) 1);
-by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
-val add_leq_self = result();
-
-goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
+goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
 by (rtac (add_commute RS ssubst) 1);
-by (REPEAT (ares_tac [add_leq_self] 1));
-val add_leq_self2 = result();
+by (REPEAT (ares_tac [add_le_self] 1));
+val add_le_self2 = result();
 
 (** Monotonicity of addition **)
 
 (*strict, in 1st argument*)
-goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
-by (etac succ_less_induct 1);
-by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
-val add_less_mono1 = result();
+goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
+by (forward_tac [lt_nat_in_nat] 1);
+ba 1;
+by (etac succ_lt_induct 1);
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
+val add_lt_mono1 = result();
 
 (*strict, in both arguments*)
-goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
-by (rtac (add_less_mono1 RS Ord_trans) 1);
-by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
+goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
+by (rtac (add_lt_mono1 RS lt_trans) 1);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
 by (EVERY [rtac (add_commute RS ssubst) 1,
 	   rtac (add_commute RS ssubst) 3,
-	   rtac add_less_mono1 5]);
-by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
-val add_less_mono = result();
+	   rtac add_lt_mono1 5]);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
+val add_lt_mono = result();
 
-(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
-val less_mono::ford::prems = goal Ord.thy
-     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
-\        !!i. i:k ==> f(i):k;			\
-\        i<=j;  i:k;  j:k;  Ord(k)		\
-\     |] ==> f(i) <= f(j)";
+(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
+val lt_mono::ford::prems = goal Ord.thy
+     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
+\        !!i. i:k ==> Ord(f(i));		\
+\        i le j;  j:k				\
+\     |] ==> f(i) le f(j)";
 by (cut_facts_tac prems 1);
-by (rtac member_succD 1);
-by (dtac member_succI 1);
-by (fast_tac (ZF_cs addSIs [less_mono]) 3);
-by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
-val Ord_less_mono_imp_mono = result();
+by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
+val Ord_lt_mono_imp_le_mono = result();
 
-(*<=, in 1st argument*)
+(*le monotonicity, 1st argument*)
 goal Arith.thy
-    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
-by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
-by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
-val add_mono1 = result();
+    "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
+by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
+val add_le_mono1 = result();
 
-(*<=, in both arguments*)
+(* le monotonicity, BOTH arguments*)
 goal Arith.thy
-    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
-by (rtac (add_mono1 RS subset_trans) 1);
-by (REPEAT (assume_tac 1));
+    "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
+by (rtac (add_le_mono1 RS le_trans) 1);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
 by (EVERY [rtac (add_commute RS ssubst) 1,
 	   rtac (add_commute RS ssubst) 3,
-	   rtac add_mono1 5]);
-by (REPEAT (assume_tac 1));
-val add_mono = result();
+	   rtac add_le_mono1 5]);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
+val add_le_mono = result();
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/Arith.thy	Tue Oct 05 15:21:29 1993 +0100
@@ -21,6 +21,6 @@
     add_def  "m#+n == rec(m, n, %u v.succ(v))"
     diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
     mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
-    mod_def  "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))"
-    div_def  "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))"
+    mod_def  "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
+    div_def  "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
 end
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/Epsilon.ML
--- a/src/ZF/Epsilon.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/Epsilon.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -195,35 +195,35 @@
 by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
 val rank_of_Ord = result();
 
-val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
+goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
-by (rtac (prem RS UN_I) 1);
+be (UN_I RS ltI) 1;
 by (rtac succI1 1);
+by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
 val rank_lt = result();
 
-val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
+val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
 by (rtac (major RS eclose_induct_down) 1);
 by (etac rank_lt 1);
-by (etac (rank_lt RS Ord_trans) 1);
+by (etac (rank_lt RS lt_trans) 1);
 by (assume_tac 1);
-by (rtac Ord_rank 1);
 val eclose_rank_lt = result();
 
-goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
+goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)";
+by (rtac subset_imp_le 1);
 by (rtac (rank RS ssubst) 1);
 by (rtac (rank RS ssubst) 1);
 by (etac UN_mono 1);
-by (rtac subset_refl 1);
+by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
 val rank_mono = result();
 
 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
 by (rtac (rank RS trans) 1);
-by (rtac equalityI 1);
-by (fast_tac ZF_cs 2);
-by (rtac UN_least 1);
-by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
-by (rtac Ord_rank 1);
-by (rtac Ord_rank 1);
+by (rtac le_asym 1);
+by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le),
+	     etac (PowD RS rank_mono RS succ_leI)] 1);
+by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le),
+	     REPEAT o rtac (Ord_rank RS Ord_succ)] 1);
 val rank_Pow = result();
 
 goal Epsilon.thy "rank(0) = 0";
@@ -236,62 +236,47 @@
 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
 by (etac succE 1);
 by (fast_tac ZF_cs 1);
-by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
+be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
 val rank_succ = result();
 
 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
 by (rtac equalityI 1);
-by (rtac (rank_mono RS UN_least) 2);
+by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
 by (etac Union_upper 2);
 by (rtac (rank RS ssubst) 1);
 by (rtac UN_least 1);
 by (etac UnionE 1);
 by (rtac subset_trans 1);
 by (etac (RepFunI RS Union_upper) 2);
-by (etac (rank_lt RS Ord_succ_subsetI) 1);
-by (rtac Ord_rank 1);
+by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
 val rank_Union = result();
 
 goal Epsilon.thy "rank(eclose(a)) = rank(a)";
-by (rtac equalityI 1);
+by (rtac le_asym 1);
 by (rtac (arg_subset_eclose RS rank_mono) 2);
 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
-by (rtac UN_least 1);
-by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
+by (rtac (Ord_rank RS UN_least_le) 1);
+by (etac (eclose_rank_lt RS succ_leI) 1);
 val rank_eclose = result();
 
-(*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
-val rank_trans = Ord_rank RSN (3, Ord_trans);
-
-goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
-by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
+goalw Epsilon.thy [Pair_def] "rank(a) < rank(<a,b>)";
+by (rtac (consI1 RS rank_lt RS lt_trans) 1);
 by (rtac (consI1 RS consI2 RS rank_lt) 1);
-by (rtac Ord_rank 1);
 val rank_pair1 = result();
 
-goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
-by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
+goalw Epsilon.thy [Pair_def] "rank(b) < rank(<a,b>)";
+by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
 by (rtac (consI1 RS consI2 RS rank_lt) 1);
-by (rtac Ord_rank 1);
 val rank_pair2 = result();
 
-goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
+goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) < rank(Inl(a))";
 by (rtac rank_pair2 1);
 val rank_Inl = result();
 
-goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
+goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) < rank(Inr(a))";
 by (rtac rank_pair2 1);
 val rank_Inr = result();
 
-val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
-by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
-by (rtac bexI 1);
-by (etac member_succD 1);
-by (rtac Ord_rank 1);
-by (assume_tac 1);
-val rank_implies_mem = result();
-
-
 (*** Corollaries of leastness ***)
 
 goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/arith.ML
--- a/src/ZF/arith.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/arith.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -42,9 +42,14 @@
     (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
 val rec_type = result();
 
-val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
+val nat_le_refl = naturals_are_ordinals RS le_refl;
+
+val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
 
-val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
+val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
+		 nat_le_refl];
+
+val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
 
 
 (** Addition **)
@@ -101,27 +106,24 @@
     (nat_ind_tac "n" prems 1),
     (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
 
-(*The conclusion is equivalent to m#-n <= m *)
 val prems = goal Arith.thy 
-    "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (etac succE 3);
+    "[| m:nat;  n:nat |] ==> m #- n le m";
+by (rtac (prems MRS diff_induct) 1);
+by (etac leE 3);
 by (ALLGOALS
     (asm_simp_tac
-     (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
-				diff_succ_succ]))));
-val diff_less_succ = result();
+     (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
+				diff_succ_succ, naturals_are_ordinals]))));
+val diff_le_self = result();
 
 (*** Simplification over add, mult, diff ***)
 
 val arith_typechecks = [add_type, mult_type, diff_type];
-val arith_rews = [add_0, add_succ,
-		  mult_0, mult_succ,
-		  diff_0, diff_0_eq_0, diff_succ_succ];
+val arith_simps = [add_0, add_succ,
+		   mult_0, mult_succ,
+		   diff_0, diff_0_eq_0, diff_succ_succ];
 
-val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
+val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
 
 (*** Addition ***)
 
@@ -223,19 +225,15 @@
   [ (nat_ind_tac "m" prems 1),
     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
 
-(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val notless::prems = goal Arith.thy
-    "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
-by (rtac (notless RS rev_mp) 1);
+(*Addition is the inverse of subtraction*)
+goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
+by (forward_tac [lt_nat_in_nat] 1);
+be nat_succI 1;
+by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (ALLGOALS (asm_simp_tac
-	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
-					 naturals_are_ordinals]))));
+by (ALLGOALS (asm_simp_tac arith_ss));
 val add_diff_inverse = result();
 
-
 (*Subtraction is the inverse of addition. *)
 val [mnat,nnat] = goal Arith.thy
     "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
@@ -252,148 +250,129 @@
 
 (*** Remainder ***)
 
-(*In ordinary notation: if 0<n and n<=m then m-n < m *)
-goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
+goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
+by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
 by (etac rev_mp 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
+by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
 val div_termination = result();
 
-val div_rls =
-    [Ord_transrec_type, apply_type, div_termination, if_type] @ 
-    nat_typechecks;
+val div_rls =	(*for mod and div*)
+    nat_typechecks @
+    [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
+     naturals_are_ordinals, not_lt_iff_le RS iffD1];
+
+val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
+			     not_lt_iff_le RS iffD2];
 
 (*Type checking depends upon termination!*)
-val prems = goalw Arith.thy [mod_def]
-    "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
-by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
+goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
+by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
 val mod_type = result();
 
-val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
-
-val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
+goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
 by (rtac (mod_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val mod_less = result();
 
-val prems = goal Arith.thy
-    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
+goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
+by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
 by (rtac (mod_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val mod_geq = result();
 
 (*** Quotient ***)
 
 (*Type checking depends upon termination!*)
-val prems = goalw Arith.thy [div_def]
-    "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
-by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
+goalw Arith.thy [div_def]
+    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
+by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
 val div_type = result();
 
-val prems = goal Arith.thy
-    "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
+goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
 by (rtac (div_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val div_less = result();
 
-val prems = goal Arith.thy
-    "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
+goal Arith.thy
+ "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
+by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
 by (rtac (div_def RS def_transrec RS trans) 1);
-by (simp_tac (div_ss addsimps prems) 1);
+by (asm_simp_tac div_ss 1);
 val div_geq = result();
 
 (*Main Result.*)
-val prems = goal Arith.thy
-    "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
-by (res_inst_tac [("i","m")] complete_induct 1);
-by (resolve_tac prems 1);
-by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
-by (ALLGOALS 
-    (asm_simp_tac
-     (arith_ss addsimps ([mod_type,div_type] @ prems @
-        [mod_less,mod_geq, div_less, div_geq,
-	 add_assoc, add_diff_inverse, div_termination]))));
+goal Arith.thy
+    "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
+by (etac complete_induct 1);
+by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
+(*case x<n*)
+by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
+(*case n le x*)
+by (asm_full_simp_tac
+     (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
+			 mod_geq, div_geq, add_assoc,
+			 div_termination RS ltD, add_diff_inverse]) 1);
 val mod_div_equality = result();
 
 
-(**** Additional theorems about "less than" ****)
-
-val [mnat,nnat] = goal Arith.thy
-    "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
-by (rtac (mnat RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
-by (rtac notI 1);
-by (etac notE 1);
-by (etac (succI1 RS Ord_trans) 1);
-by (rtac (nnat RS naturals_are_ordinals) 1);
-val add_not_less_self = result();
+(**** Additional theorems about "le" ****)
 
-val [mnat,nnat] = goal Arith.thy
-    "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
-by (rtac (mnat RS nat_induct) 1);
-(*May not simplify even with ZF_ss because it would expand m:succ(...) *)
-by (rtac (add_0 RS ssubst) 1);
-by (rtac (add_succ RS ssubst) 2);
-by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
-		      naturals_are_ordinals, nat_succI, add_type] 1));
-val add_less_succ_self = result();
+goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+val add_le_self = result();
 
-goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
-by (rtac (add_less_succ_self RS member_succD) 1);
-by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
-val add_leq_self = result();
-
-goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
+goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
 by (rtac (add_commute RS ssubst) 1);
-by (REPEAT (ares_tac [add_leq_self] 1));
-val add_leq_self2 = result();
+by (REPEAT (ares_tac [add_le_self] 1));
+val add_le_self2 = result();
 
 (** Monotonicity of addition **)
 
 (*strict, in 1st argument*)
-goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
-by (etac succ_less_induct 1);
-by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
-val add_less_mono1 = result();
+goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
+by (forward_tac [lt_nat_in_nat] 1);
+ba 1;
+by (etac succ_lt_induct 1);
+by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
+val add_lt_mono1 = result();
 
 (*strict, in both arguments*)
-goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
-by (rtac (add_less_mono1 RS Ord_trans) 1);
-by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
+goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
+by (rtac (add_lt_mono1 RS lt_trans) 1);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
 by (EVERY [rtac (add_commute RS ssubst) 1,
 	   rtac (add_commute RS ssubst) 3,
-	   rtac add_less_mono1 5]);
-by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
-val add_less_mono = result();
+	   rtac add_lt_mono1 5]);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
+val add_lt_mono = result();
 
-(*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
-val less_mono::ford::prems = goal Ord.thy
-     "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
-\        !!i. i:k ==> f(i):k;			\
-\        i<=j;  i:k;  j:k;  Ord(k)		\
-\     |] ==> f(i) <= f(j)";
+(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
+val lt_mono::ford::prems = goal Ord.thy
+     "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
+\        !!i. i:k ==> Ord(f(i));		\
+\        i le j;  j:k				\
+\     |] ==> f(i) le f(j)";
 by (cut_facts_tac prems 1);
-by (rtac member_succD 1);
-by (dtac member_succI 1);
-by (fast_tac (ZF_cs addSIs [less_mono]) 3);
-by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
-val Ord_less_mono_imp_mono = result();
+by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
+val Ord_lt_mono_imp_le_mono = result();
 
-(*<=, in 1st argument*)
+(*le monotonicity, 1st argument*)
 goal Arith.thy
-    "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
-by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
-by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
-val add_mono1 = result();
+    "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
+by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
+val add_le_mono1 = result();
 
-(*<=, in both arguments*)
+(* le monotonicity, BOTH arguments*)
 goal Arith.thy
-    "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
-by (rtac (add_mono1 RS subset_trans) 1);
-by (REPEAT (assume_tac 1));
+    "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
+by (rtac (add_le_mono1 RS le_trans) 1);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
 by (EVERY [rtac (add_commute RS ssubst) 1,
 	   rtac (add_commute RS ssubst) 3,
-	   rtac add_mono1 5]);
-by (REPEAT (assume_tac 1));
-val add_mono = result();
+	   rtac add_le_mono1 5]);
+by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
+val add_le_mono = result();
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/arith.thy
--- a/src/ZF/arith.thy	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/arith.thy	Tue Oct 05 15:21:29 1993 +0100
@@ -21,6 +21,6 @@
     add_def  "m#+n == rec(m, n, %u v.succ(v))"
     diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
     mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
-    mod_def  "m mod n == transrec(m, %j f. if(j:n, j, f`(j#-n)))"
-    div_def  "m div n == transrec(m, %j f. if(j:n, 0, succ(f`(j#-n))))"
+    mod_def  "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
+    div_def  "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
 end
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/epsilon.ML
--- a/src/ZF/epsilon.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/epsilon.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -195,35 +195,35 @@
 by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
 val rank_of_Ord = result();
 
-val [prem] = goal Epsilon.thy "a:b ==> rank(a) : rank(b)";
+goal Epsilon.thy "!!a b. a:b ==> rank(a) < rank(b)";
 by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
-by (rtac (prem RS UN_I) 1);
+be (UN_I RS ltI) 1;
 by (rtac succI1 1);
+by (REPEAT (ares_tac [Ord_UN, Ord_succ, Ord_rank] 1));
 val rank_lt = result();
 
-val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) : rank(b)";
+val [major] = goal Epsilon.thy "a: eclose(b) ==> rank(a) < rank(b)";
 by (rtac (major RS eclose_induct_down) 1);
 by (etac rank_lt 1);
-by (etac (rank_lt RS Ord_trans) 1);
+by (etac (rank_lt RS lt_trans) 1);
 by (assume_tac 1);
-by (rtac Ord_rank 1);
 val eclose_rank_lt = result();
 
-goal Epsilon.thy "!!a b. a<=b ==> rank(a) <= rank(b)";
+goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)";
+by (rtac subset_imp_le 1);
 by (rtac (rank RS ssubst) 1);
 by (rtac (rank RS ssubst) 1);
 by (etac UN_mono 1);
-by (rtac subset_refl 1);
+by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
 val rank_mono = result();
 
 goal Epsilon.thy "rank(Pow(a)) = succ(rank(a))";
 by (rtac (rank RS trans) 1);
-by (rtac equalityI 1);
-by (fast_tac ZF_cs 2);
-by (rtac UN_least 1);
-by (etac (PowD RS rank_mono RS Ord_succ_mono) 1);
-by (rtac Ord_rank 1);
-by (rtac Ord_rank 1);
+by (rtac le_asym 1);
+by (DO_GOAL [rtac (Ord_rank RS Ord_succ RS UN_least_le),
+	     etac (PowD RS rank_mono RS succ_leI)] 1);
+by (DO_GOAL [rtac ([Pow_top, le_refl] MRS UN_upper_le),
+	     REPEAT o rtac (Ord_rank RS Ord_succ)] 1);
 val rank_Pow = result();
 
 goal Epsilon.thy "rank(0) = 0";
@@ -236,62 +236,47 @@
 by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
 by (etac succE 1);
 by (fast_tac ZF_cs 1);
-by (REPEAT (ares_tac [Ord_succ_mono,Ord_rank,OrdmemD,rank_lt] 1));
+be (rank_lt RS leI RS succ_leI RS le_imp_subset) 1;
 val rank_succ = result();
 
 goal Epsilon.thy "rank(Union(A)) = (UN x:A. rank(x))";
 by (rtac equalityI 1);
-by (rtac (rank_mono RS UN_least) 2);
+by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
 by (etac Union_upper 2);
 by (rtac (rank RS ssubst) 1);
 by (rtac UN_least 1);
 by (etac UnionE 1);
 by (rtac subset_trans 1);
 by (etac (RepFunI RS Union_upper) 2);
-by (etac (rank_lt RS Ord_succ_subsetI) 1);
-by (rtac Ord_rank 1);
+by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
 val rank_Union = result();
 
 goal Epsilon.thy "rank(eclose(a)) = rank(a)";
-by (rtac equalityI 1);
+by (rtac le_asym 1);
 by (rtac (arg_subset_eclose RS rank_mono) 2);
 by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
-by (rtac UN_least 1);
-by (etac ([eclose_rank_lt, Ord_rank] MRS Ord_succ_subsetI) 1);
+by (rtac (Ord_rank RS UN_least_le) 1);
+by (etac (eclose_rank_lt RS succ_leI) 1);
 val rank_eclose = result();
 
-(*  [| i: j; j: rank(a) |] ==> i: rank(a)  *)
-val rank_trans = Ord_rank RSN (3, Ord_trans);
-
-goalw Epsilon.thy [Pair_def] "rank(a) : rank(<a,b>)";
-by (rtac (consI1 RS rank_lt RS Ord_trans) 1);
+goalw Epsilon.thy [Pair_def] "rank(a) < rank(<a,b>)";
+by (rtac (consI1 RS rank_lt RS lt_trans) 1);
 by (rtac (consI1 RS consI2 RS rank_lt) 1);
-by (rtac Ord_rank 1);
 val rank_pair1 = result();
 
-goalw Epsilon.thy [Pair_def] "rank(b) : rank(<a,b>)";
-by (rtac (consI1 RS consI2 RS rank_lt RS Ord_trans) 1);
+goalw Epsilon.thy [Pair_def] "rank(b) < rank(<a,b>)";
+by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
 by (rtac (consI1 RS consI2 RS rank_lt) 1);
-by (rtac Ord_rank 1);
 val rank_pair2 = result();
 
-goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) : rank(Inl(a))";
+goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inl_def] "rank(a) < rank(Inl(a))";
 by (rtac rank_pair2 1);
 val rank_Inl = result();
 
-goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) : rank(Inr(a))";
+goalw (merge_theories(Epsilon.thy,Sum.thy)) [Inr_def] "rank(a) < rank(Inr(a))";
 by (rtac rank_pair2 1);
 val rank_Inr = result();
 
-val [major] = goal Epsilon.thy "i: rank(a) ==> (EX x:a. i<=rank(x))";
-by (resolve_tac ([major] RL [rank RS subst] RL [UN_E]) 1);
-by (rtac bexI 1);
-by (etac member_succD 1);
-by (rtac Ord_rank 1);
-by (assume_tac 1);
-val rank_implies_mem = result();
-
-
 (*** Corollaries of leastness ***)
 
 goal Epsilon.thy "!!A B. A:B ==> eclose(A)<=eclose(B)";
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/intr-elim.ML
--- a/src/ZF/intr-elim.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/intr-elim.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -19,7 +19,7 @@
   where M is some monotone operator (usually the identity)
   P(x) is any (non-conjunctive) side condition on the free variables
   ti, t are any terms
-  Sj, Sk are two of the sets being defiend in mutual recursion
+  Sj, Sk are two of the sets being defined in mutual recursion
 
 Sums are used only for mutual recursion;
 Products are used only to derive "streamlined" induction rules for relations
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/intr_elim.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -19,7 +19,7 @@
   where M is some monotone operator (usually the identity)
   P(x) is any (non-conjunctive) side condition on the free variables
   ti, t are any terms
-  Sj, Sk are two of the sets being defiend in mutual recursion
+  Sj, Sk are two of the sets being defined in mutual recursion
 
 Sums are used only for mutual recursion;
 Products are used only to derive "streamlined" induction rules for relations
diff -r f3d4ff75d9f2 -r 3ac1c0c0016e src/ZF/listfn.ML
--- a/src/ZF/listfn.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/listfn.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -59,7 +59,7 @@
 
 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
 by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
+by (simp_tac (rank_ss addsimps (rank_Cons2::List.case_eqns)) 1);
 val list_rec_Cons = result();
 
 (*Type checking -- proved by induction, as usual*)