# HG changeset patch
# User lcp
# Date 749831549 -3600
# Node ID 5aa9c39b480d1ebc5e33edd38350357ffd2e3da9
# Parent  3ac1c0c0016eb4aa7b9460f49ce71827f6824587
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 3ac1c0c0016e -r 5aa9c39b480d src/ZF/ListFn.ML
--- a/src/ZF/ListFn.ML	Tue Oct 05 15:21:29 1993 +0100
+++ b/src/ZF/ListFn.ML	Tue Oct 05 15:32: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*)