src/FOLP/intprover.ML
changeset 2603 4988dda71c0b
parent 2572 8a47f85e7a03
child 4440 9ed4098074bc
     1.1 --- a/src/FOLP/intprover.ML	Mon Feb 10 12:34:54 1997 +0100
     1.2 +++ b/src/FOLP/intprover.ML	Mon Feb 10 12:52:11 1997 +0100
     1.3 @@ -5,12 +5,12 @@
     1.4  
     1.5  A naive prover for intuitionistic logic
     1.6  
     1.7 -BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ...
     1.8 +BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
     1.9  
    1.10  Completeness (for propositional logic) is proved in 
    1.11  
    1.12  Roy Dyckhoff.
    1.13 -Contraction-Free Sequent Calculi for Intuitionistic Logic.
    1.14 +Contraction-Free Sequent Calculi for IntPruitionistic Logic.
    1.15  J. Symbolic Logic (in press)
    1.16  *)
    1.17  
    1.18 @@ -27,7 +27,7 @@
    1.19    end;
    1.20  
    1.21  
    1.22 -structure Int : INT_PROVER   = 
    1.23 +structure IntPr : INT_PROVER   = 
    1.24  struct
    1.25  
    1.26  (*Negation is treated as a primitive symbol, with rules notI (introduction),