# HG changeset patch
# User ballarin
# Date 1038494674 -3600
# Node ID 6ea0e7c43c4fbdd4cd085168e7ee2df217e7d8c5
# Parent  7de9342aca7a2cecb4cfafb166afcb5d624523bf
Transitivity reasoner renamed to linorder.ML.  README updated.

diff -r 7de9342aca7a -r 6ea0e7c43c4f src/Provers/README
--- 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: