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/Finite.thy
changeset 13615 449a70d88b38
parent 13524 604d0f3622d6
child 13784 b9f6154427a4 
--- a/src/ZF/Finite.thy	Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Finite.thy	Tue Oct 01 13:26:10 2002 +0200
@@ -172,7 +172,6 @@
 apply (erule Fin.induct)
  apply (simp add: FiniteFun.intros, clarify)
 apply (case_tac "a:b")
- apply (rotate_tac -1)
  apply (simp add: cons_absorb)
 apply (subgoal_tac "restrict (f,b) : b -||> B")
  prefer 2 apply (blast intro: restrict_type2)
isabelle