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