src/Provers/README
changeset 38052 04a8de29e8f7
parent 30159 7b55b6b5c0c2
equal deleted inserted replaced
38031:ac704f1c8dde 38052:04a8de29e8f7
    11   quantifier1.ML	simplification procedures for "1 point rules"
    11   quantifier1.ML	simplification procedures for "1 point rules"
    12   splitter.ML           performs case splits for simplifier
    12   splitter.ML           performs case splits for simplifier
    13   typedsimp.ML          basic simplifier for explicitly typed logics
    13   typedsimp.ML          basic simplifier for explicitly typed logics
    14 
    14 
    15 directory Arith:
    15 directory Arith:
    16   abel_cancel.ML	cancel complementary terms in sums of Abelian groups
       
    17   assoc_fold.ML		fold numerals in nested products
    16   assoc_fold.ML		fold numerals in nested products
    18   cancel_numerals.ML	cancel common coefficients in balanced expressions
    17   cancel_numerals.ML	cancel common coefficients in balanced expressions
    19   cancel_factor.ML	cancel common constant factor
       
    20   cancel_sums.ML	cancel common summands
    18   cancel_sums.ML	cancel common summands
    21   combine_numerals.ML	combine coefficients in expressions
    19   combine_numerals.ML	combine coefficients in expressions
    22   fast_lin_arith.ML	generic linear arithmetic package
    20   fast_lin_arith.ML	generic linear arithmetic package