# HG changeset patch
# User paulson
# Date 968141462 -7200
# Node ID 543d23cd1259135add27245343cc33337f1c2888
# Parent  109b11c4e77eaabf21f125a70c518e9fb9dbd6cc
meson_tac

diff -r 109b11c4e77e -r 543d23cd1259 NEWS
--- a/NEWS	Tue Sep 05 09:03:17 2000 +0200
+++ b/NEWS	Tue Sep 05 10:11:02 2000 +0200
@@ -256,6 +256,10 @@
   and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
     or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
 
+* HOL: meson_tac is available (previously in ex/meson.ML).  It is a powerful
+   prover for predicate logic but knows nothing of clasets.  For examples of
+   what it can do, see ex/mesontest.ML and ex/mesontest2.ML;
+
 * HOL: new version of "case_tac" subsumes both boolean case split and
 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
 exists, may define val exhaust_tac = case_tac for ad-hoc portability;