src/FOLP/IFOLP.thy

   shows "?p:Q"
   apply (assumption | rule assms impI notE)+
   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