--- a/src/ZF/Constructible/WFrec.thy Tue Oct 01 11:17:25 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Tue Oct 01 13:26:10 2002 +0200
@@ -143,7 +143,7 @@
apply (drule equalityD1 [THEN subsetD], assumption)
apply (blast dest: pair_components_in_M)
apply (blast elim!: equalityE dest: pair_components_in_M)
- apply (frule transM, assumption, rotate_tac -1)
+ apply (frule transM, assumption)
apply simp
apply blast
apply (subgoal_tac "is_function(M,f)")
@@ -187,7 +187,6 @@
apply (frule pair_components_in_M, assumption, clarify)
apply (rule iffI)
apply (frule_tac y="<y,z>" in transM, assumption)
- apply (rotate_tac -1)
apply (clarsimp simp add: vimage_singleton_iff is_recfun_type [THEN apply_iff]
apply_recfun is_recfun_cut)
txt{*Opposite inclusion: something in f, show in Y*}
@@ -320,9 +319,7 @@
relativize2(M,MH,H); M(r)|]
==> strong_replacement(M, \<lambda>x z. \<exists>y[M].
pair(M,x,y,z) & (\<exists>g[M]. is_recfun(r,x,H,g) & y = H(x,g)))"
-apply (rotate_tac 1)
-apply (simp add: wfrec_replacement_def is_wfrec_abs)
-done
+by (simp add: wfrec_replacement_def is_wfrec_abs)
lemma wfrec_replacement_cong [cong]:
"[| !!x y z. [| M(x); M(y); M(z) |] ==> MH(x,y,z) <-> MH'(x,y,z);