--- 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),