src/Provers/README
changeset 16019 0e1405402d53
parent 13736 6ea0e7c43c4f
child 30159 7b55b6b5c0c2
equal deleted inserted replaced
16018:3e4e077af2e7 16019:0e1405402d53
    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   induct_method.ML      proof by cases and induction on sets and types (Isar)
    14   linorder.ML		transitivity reasoner for linear (total) orders
    14   linorder.ML		transitivity reasoner for linear (total) orders
    15   quantifier1.ML	simplification procedures for "1 point rules"
    15   quantifier1.ML	simplification procedures for "1 point rules"
    16   simp.ML               powerful but slow simplifier
    16   simp.ML               powerful but slow simplifier
    17   simplifier.ML         fast simplifier
       
    18   split_paired_all.ML	turn surjective pairing into split rule
    17   split_paired_all.ML	turn surjective pairing into split rule
    19   splitter.ML           performs case splits for simplifier.ML
    18   splitter.ML           performs case splits for simplifier
    20   typedsimp.ML          basic simplifier for explicitly typed logics
    19   typedsimp.ML          basic simplifier for explicitly typed logics
    21 
    20 
    22 directory Arith:
    21 directory Arith:
    23   abel_cancel.ML	cancel complementary terms in sums of Abelian groups
    22   abel_cancel.ML	cancel complementary terms in sums of Abelian groups
    24   assoc_fold.ML		fold numerals in nested products
    23   assoc_fold.ML		fold numerals in nested products