src/ZF/Constructible/Relative.thy
changeset 13543 2b3c7e319d82
parent 13535 007559e981c7
child 13563 7d6c9817c432
     1.1 --- a/src/ZF/Constructible/Relative.thy	Tue Aug 27 17:25:44 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Relative.thy	Wed Aug 28 13:08:34 2002 +0200
     1.3 @@ -819,8 +819,9 @@
     1.4  by (simp add: ordinal_def Ord_def)
     1.5  
     1.6  lemma (in M_triv_axioms) limit_ordinal_abs [simp]: 
     1.7 -     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
     1.8 -apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def) 
     1.9 +     "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" 
    1.10 +apply (unfold Limit_def limit_ordinal_def) 
    1.11 +apply (simp add: Ord_0_lt_iff) 
    1.12  apply (simp add: lt_def, blast) 
    1.13  done
    1.14