--- a/src/Provers/README Thu Nov 28 10:50:42 2002 +0100
+++ b/src/Provers/README Thu Nov 28 15:44:34 2002 +0100
@@ -11,12 +11,12 @@
hypsubst.ML tactic to substitute in the hypotheses
ind.ML a simple induction package
induct_method.ML proof by cases and induction on sets and types (Isar)
+ linorder.ML transitivity reasoner for linear (total) orders
quantifier1.ML simplification procedures for "1 point rules"
simp.ML powerful but slow simplifier
simplifier.ML fast simplifier
split_paired_all.ML turn surjective pairing into split rule
splitter.ML performs case splits for simplifier.ML
- trans.ML transitivity reasoner for linear (total) orders
typedsimp.ML basic simplifier for explicitly typed logics
directory Arith: