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 |