Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Constructible/Normal.thy
changeset 13268 240509babf00
parent 13223 45be08fbdcff
child 13382 b37764a46b16 
--- a/src/ZF/Constructible/Normal.thy	Mon Jul 01 18:10:53 2002 +0200
+++ b/src/ZF/Constructible/Normal.thy	Mon Jul 01 18:16:18 2002 +0200
@@ -316,8 +316,7 @@
    --"this lemma is @{thm increasing_LimitI [no_vars]}"
  apply (blast intro: UN_upper_lt [of "1"]   Normal_imp_Ord
                      Ord_UN Ord_iterates lt_imp_0_lt
-                     iterates_Normal_increasing)
-apply clarify
+                     iterates_Normal_increasing, clarify)
 apply (rule bexI) 
  apply (blast intro: Ord_in_Ord [OF Ord_iterates_Normal]) 
 apply (rule UN_I, erule nat_succI)
isabelle