--- a/src/ZF/WF.thy Wed May 22 19:34:01 2002 +0200
+++ b/src/ZF/WF.thy Thu May 23 17:05:21 2002 +0200
@@ -213,8 +213,9 @@
lemma apply_recfun:
"[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
apply (unfold is_recfun_def)
-apply (erule_tac P = "%x.?t (x) = (?u::i) " in ssubst)
-apply (erule underI [THEN beta])
+ txt{*replace f only on the left-hand side*}
+apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
+apply (simp add: underI);
done
lemma is_recfun_equal [rule_format]:
@@ -280,7 +281,7 @@
apply (frule spec [THEN mp], assumption)
apply (subgoal_tac "<xa,a1> : r")
apply (drule_tac x1 = "xa" in spec [THEN mp], assumption)
-apply (simp add: vimage_singleton_iff underI [THEN beta]
+apply (simp add: vimage_singleton_iff
apply_recfun is_recfun_cut)
apply (blast dest: transD)
done