# HG changeset patch
# User wenzelm
# Date 1213191717 -7200
# Node ID a42aef558ce3e5410fab12c4799daf5d489664bc
# Parent  123377499a8ed43cee884ec86d59f8bc80f4c882
tuned comments;

diff -r 123377499a8e -r a42aef558ce3 src/FOL/IFOL.thy
--- 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)
 
diff -r 123377499a8e -r a42aef558ce3 src/FOLP/IFOLP.thy
--- 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
diff -r 123377499a8e -r a42aef558ce3 src/ZF/AC/WO6_WO1.thy
--- 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
 
diff -r 123377499a8e -r a42aef558ce3 src/ZF/func.thy
--- 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)