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)