# 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   *)