equal
deleted
inserted
replaced
4 Typically, they can be applied to various logics, provided rules of a 
4 Typically, they can be applied to various logics, provided rules of a 
5 certain form are derivable. Some of these are documented in the 
5 certain form are derivable. Some of these are documented in the 
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 classical.ML theorem prover for classical logics 
10 classical.ML theorem prover for classical logics 
10 genelim.ML bits and pieces for deriving elimination rules 
11 genelim.ML bits and pieces for deriving elimination rules 
11 hypsubst.ML tactic to substitute in the hypotheses 
12 hypsubst.ML tactic to substitute in the hypotheses 
12 ind.ML a simple induction package 
13 ind.ML a simple induction package 
13 quantifier1.ML simplification procedures for "1 point rules" 
14 quantifier1.ML simplification procedures for "1 point rules" 