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