equal
deleted
inserted
replaced
12 hypsubst.ML tactic to substitute in the hypotheses |
12 hypsubst.ML tactic to substitute in the hypotheses |
13 ind.ML a simple induction package |
13 ind.ML a simple induction package |
14 quantifier1.ML simplification procedures for "1 point rules" |
14 quantifier1.ML simplification procedures for "1 point rules" |
15 simp.ML powerful but slow simplifier |
15 simp.ML powerful but slow simplifier |
16 simplifier.ML fast simplifier |
16 simplifier.ML fast simplifier |
|
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 |
18 typedsimp.ML basic simplifier for explicitly typed logics |
19 typedsimp.ML basic simplifier for explicitly typed logics |
19 |
20 |
20 directory Arith: |
21 directory Arith: |
21 cancel_factor.ML cancel common constant factor |
22 cancel_factor.ML cancel common constant factor |