--- a/src/ZF/Constructible/Relative.thy Tue Aug 27 17:25:44 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Wed Aug 28 13:08:34 2002 +0200
@@ -819,8 +819,9 @@
by (simp add: ordinal_def Ord_def)
lemma (in M_triv_axioms) limit_ordinal_abs [simp]:
- "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
-apply (simp add: limit_ordinal_def Ord_0_lt_iff Limit_def)
+ "M(a) ==> limit_ordinal(M,a) <-> Limit(a)"
+apply (unfold Limit_def limit_ordinal_def)
+apply (simp add: Ord_0_lt_iff)
apply (simp add: lt_def, blast)
done