# HG changeset patch
# User wenzelm
# Date 1235825687 -3600
# Node ID 7b55b6b5c0c2561eb509a1ee91c8cbdd37318d83
# Parent  83c50c62cf23acb3ac0522a14686242d2b8ae8d4
some updates on ancient README;

diff -r 83c50c62cf23 -r 7b55b6b5c0c2 src/Provers/README
--- a/src/Provers/README	Fri Feb 27 19:05:46 2009 -0800
+++ b/src/Provers/README	Sat Feb 28 13:54:47 2009 +0100
@@ -2,19 +2,13 @@
 
 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.  Some of these are documented in the
-Reference Manual.
+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
-  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
-  split_paired_all.ML	turn surjective pairing into split rule
   splitter.ML           performs case splits for simplifier
   typedsimp.ML          basic simplifier for explicitly typed logics