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/AC_in_L.thy
changeset 13615 449a70d88b38
parent 13546 f76237c2be75
child 13634 99a593b49b04 
--- a/src/ZF/Constructible/AC_in_L.thy	Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/AC_in_L.thy	Tue Oct 01 13:26:10 2002 +0200
@@ -240,7 +240,6 @@
  apply safe
  apply (subgoal_tac "Ord(y)")
   prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord)
- apply (rotate_tac -1) 
  apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
                       Ord_mem_iff_lt) 
  apply (blast intro: lt_trans)
isabelle