--- a/src/FOL/IFOL.thy Wed Jun 11 15:41:33 2008 +0200
+++ b/src/FOL/IFOL.thy Wed Jun 11 15:41:57 2008 +0200
@@ -226,9 +226,7 @@
done
(* For substitution into an assumption P, reduce Q to P-->Q, substitute into
- this implication, then apply impI to move P back into the assumptions.
- To specify P use something like
- eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *)
+ this implication, then apply impI to move P back into the assumptions.*)
lemma rev_mp: "[| P; P --> Q |] ==> Q"
by (erule mp)
--- a/src/FOLP/IFOLP.thy Wed Jun 11 15:41:33 2008 +0200
+++ b/src/FOLP/IFOLP.thy Wed Jun 11 15:41:57 2008 +0200
@@ -216,9 +216,7 @@
done
(* For substitution int an assumption P, reduce Q to P-->Q, substitute into
- this implication, then apply impI to move P back into the assumptions.
- To specify P use something like
- eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *)
+ this implication, then apply impI to move P back into the assumptions.*)
lemma rev_mp: "[| p:P; q:P --> Q |] ==> ?p:Q"
apply (assumption | rule mp)+
done
--- a/src/ZF/AC/WO6_WO1.thy Wed Jun 11 15:41:33 2008 +0200
+++ b/src/ZF/AC/WO6_WO1.thy Wed Jun 11 15:41:57 2008 +0200
@@ -395,8 +395,6 @@
apply (erule succ_natD)
apply (rule_tac x = "a++a" in exI)
apply (rule_tac x = "gg2 (f,a,b,x) " in exI)
-(*Calling fast_tac might get rid of the res_inst_tac calls, but it
- is just too slow.*)
apply (simp add: Ord_oadd domain_gg2 UN_gg2_eq gg2_lepoll_m)
done
--- a/src/ZF/func.thy Wed Jun 11 15:41:33 2008 +0200
+++ b/src/ZF/func.thy Wed Jun 11 15:41:57 2008 +0200
@@ -90,7 +90,7 @@
apply (blast intro: function_apply_Pair)
done
-(*Conclusion is flexible -- use res_inst_tac or else apply_funtype below!*)
+(*Conclusion is flexible -- use rule_tac or else apply_funtype below!*)
lemma apply_type [TC]: "[| f: Pi(A,B); a:A |] ==> f`a : B(a)"
by (blast intro: apply_Pair dest: fun_is_rel)