# HG changeset patch # User lcp # Date 797158736 -7200 # Node ID 280ec187f8e1d3127d2d37132c1d194e3cd2e02d # Parent 1f416fb5de91e9d5c3cb37c23e3232ab6d267340 Fixed typo. diff -r 1f416fb5de91 -r 280ec187f8e1 src/FOL/IFOL.ML --- a/src/FOL/IFOL.ML Thu Apr 06 10:56:39 1995 +0200 +++ b/src/FOL/IFOL.ML Thu Apr 06 10:58:56 1995 +0200 @@ -51,8 +51,7 @@ "[| ~P; (P-->False) ==> Q |] ==> Q" (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); - -(* For substitution int an assumption P, reduce Q to P-->Q, substitute into +(* 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 *)