src/Provers/README
changeset 5897 b3548f939dd2
parent 5680 4f526bcd3a68
child 8870 e900a58cafe4
equal deleted inserted replaced
5896:4a75d89e2818 5897:b3548f939dd2
     6 Reference Manual.
     6 Reference Manual.
     7 
     7 
     8   blast.ML              generic tableau prover with proof reconstruction
     8   blast.ML              generic tableau prover with proof reconstruction
     9   clasimp.ML		combination of classical reasoner and simplifier
     9   clasimp.ML		combination of classical reasoner and simplifier
    10   classical.ML          theorem prover for classical logics
    10   classical.ML          theorem prover for classical logics
    11   genelim.ML            bits and pieces for deriving elimination rules
       
    12   hypsubst.ML           tactic to substitute in the hypotheses
    11   hypsubst.ML           tactic to substitute in the hypotheses
    13   ind.ML                a simple induction package
    12   ind.ML                a simple induction package
    14   quantifier1.ML	simplification procedures for "1 point rules"
    13   quantifier1.ML	simplification procedures for "1 point rules"
    15   simp.ML               powerful but slow simplifier
    14   simp.ML               powerful but slow simplifier
    16   simplifier.ML         fast simplifier
    15   simplifier.ML         fast simplifier