src/FOL/intprover.ML
changeset 2601 b301958c465d
parent 2572 8a47f85e7a03
child 4440 9ed4098074bc
--- a/src/FOL/intprover.ML	Fri Feb 07 17:15:30 1997 +0100
+++ b/src/FOL/intprover.ML	Mon Feb 10 12:31:54 1997 +0100
@@ -5,7 +5,7 @@
 
 A naive prover for intuitionistic logic
 
-BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ...
+BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
 
 Completeness (for propositional logic) is proved in 
 
@@ -29,7 +29,7 @@
   end;
 
 
-structure Int : INT_PROVER   = 
+structure IntPr : INT_PROVER   = 
 struct
 
 (*Negation is treated as a primitive symbol, with rules notI (introduction),