--- a/src/HOL/NumberTheory/BijectionRel.thy Mon Oct 07 19:01:51 2002 +0200
+++ b/src/HOL/NumberTheory/BijectionRel.thy Tue Oct 08 08:20:17 2002 +0200
@@ -191,7 +191,6 @@
apply clarify
apply (case_tac "b \<in> F")
prefer 2
- apply (rotate_tac -1)
apply (simp add: subset_insert)
apply (cut_tac F = F and a = b and A = A and B = B in aux1)
prefer 6
@@ -205,7 +204,6 @@
apply clarify
apply (case_tac "a \<in> F")
apply (case_tac [!] "b \<in> F")
- apply (rotate_tac [2-4] -2)
apply (cut_tac F = F and a = a and b = b and A = A and B = B
in aux2)
apply (simp_all add: subset_insert)