src/Provers/README

added "mono" attribute to BNF generated pred_mono theorems

+
−                 Provers: generic theorem proving tools
+
−
+
−This directory contains ML sources of generic theorem proving tools.
+
−Typically, they can be applied to various logics, provided rules of a
+
−certain form are derivable.
+
−
+
−  blast.ML              generic tableau prover with proof reconstruction
+
−  clasimp.ML		combination of classical reasoner and simplifier
+
−  classical.ML          theorem prover for classical logics
+
−  hypsubst.ML           tactic to substitute in the hypotheses
+
−  quantifier1.ML	simplification procedures for "1 point rules"
+
−  splitter.ML           performs case splits for simplifier
+
−  typedsimp.ML          basic simplifier for explicitly typed logics
+
−
+
−directory Arith:
+
−  assoc_fold.ML		fold numerals in nested products
+
−  cancel_numerals.ML	cancel common coefficients in balanced expressions
+
−  cancel_sums.ML	cancel common summands
+
−  combine_numerals.ML	combine coefficients in expressions
+
−  fast_lin_arith.ML	generic linear arithmetic package