equal
deleted
inserted
replaced
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 hypsubst.ML tactic to substitute in the hypotheses 
11 hypsubst.ML tactic to substitute in the hypotheses 
12 ind.ML a simple induction package 
12 ind.ML a simple induction package 

13 induct_method.ML proof by cases and induction on sets and types (Isar) 
13 quantifier1.ML simplification procedures for "1 point rules" 
14 quantifier1.ML simplification procedures for "1 point rules" 
14 simp.ML powerful but slow simplifier 
15 simp.ML powerful but slow simplifier 
15 simplifier.ML fast simplifier 
16 simplifier.ML fast simplifier 
16 split_paired_all.ML turn surjective pairing into split rule 
17 split_paired_all.ML turn surjective pairing into split rule 
17 splitter.ML performs case splits for simplifier.ML 
18 splitter.ML performs case splits for simplifier.ML 