--- a/src/FOLP/intprover.ML Mon Feb 10 12:34:54 1997 +0100
+++ b/src/FOLP/intprover.ML Mon Feb 10 12:52:11 1997 +0100
@@ -5,12 +5,12 @@
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
Roy Dyckhoff.
-Contraction-Free Sequent Calculi for Intuitionistic Logic.
+Contraction-Free Sequent Calculi for IntPruitionistic Logic.
J. Symbolic Logic (in press)
*)
@@ -27,7 +27,7 @@
end;
-structure Int : INT_PROVER =
+structure IntPr : INT_PROVER =
struct
(*Negation is treated as a primitive symbol, with rules notI (introduction),