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

--- 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*)