changeset 5897 | b3548f939dd2 |
parent 5680 | 4f526bcd3a68 |
child 8870 | e900a58cafe4 |
--- a/src/Provers/README Mon Nov 16 11:33:42 1998 +0100 +++ b/src/Provers/README Mon Nov 16 13:54:35 1998 +0100 @@ -8,7 +8,6 @@ blast.ML generic tableau prover with proof reconstruction clasimp.ML combination of classical reasoner and simplifier classical.ML theorem prover for classical logics - genelim.ML bits and pieces for deriving elimination rules hypsubst.ML tactic to substitute in the hypotheses ind.ML a simple induction package quantifier1.ML simplification procedures for "1 point rules"