equal
deleted
inserted
replaced
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 split_paired_all.ML turn surjective pairing into split rule |
18 splitter.ML performs case splits for simplifier.ML |
18 splitter.ML performs case splits for simplifier.ML |
|
19 trans.ML transitivity reasoner for linear (total) orders |
19 typedsimp.ML basic simplifier for explicitly typed logics |
20 typedsimp.ML basic simplifier for explicitly typed logics |
20 |
21 |
21 directory Arith: |
22 directory Arith: |
22 abel_cancel.ML cancel complementary terms in sums of Abelian groups |
23 abel_cancel.ML cancel complementary terms in sums of Abelian groups |
23 assoc_fold.ML fold numerals in nested products |
24 assoc_fold.ML fold numerals in nested products |