src/Provers/README
changeset 8870 e900a58cafe4
parent 5897 b3548f939dd2
child 11840 54fe56353704
equal deleted inserted replaced
8869:9ba7ef8a765b 8870:e900a58cafe4
    16   split_paired_all.ML	turn surjective pairing into split rule
    16   split_paired_all.ML	turn surjective pairing into split rule
    17   splitter.ML           performs case splits for simplifier.ML
    17   splitter.ML           performs case splits for simplifier.ML
    18   typedsimp.ML          basic simplifier for explicitly typed logics
    18   typedsimp.ML          basic simplifier for explicitly typed logics
    19 
    19 
    20 directory Arith:
    20 directory Arith:
       
    21   abel_cancel.ML	cancel complementary terms in sums of Abelian groups
       
    22   assoc_fold.ML		fold numerals in nested products
       
    23   cancel_numerals.ML	cancel common coefficients in balanced expressions
    21   cancel_factor.ML	cancel common constant factor
    24   cancel_factor.ML	cancel common constant factor
    22   cancel_sums.ML	cancel common summands
    25   cancel_sums.ML	cancel common summands
    23   nat_transitive.ML	simple package for inequalities over nat
    26   combine_numerals.ML	combine coefficients in expressions
       
    27   fast_lin_arith.ML	generic linear arithmetic package