# HG changeset patch
# User paulson
# Date 935068932 -7200
# Node ID d603a06b30df9f456b36fcb0853767f87bb4f316
# Parent  fcbf147e7b4c947e47ee6488ec980b5e2c0b8228
defer_recdef

diff -r fcbf147e7b4c -r d603a06b30df NEWS
--- a/NEWS	Thu Aug 19 15:13:37 1999 +0200
+++ b/NEWS	Thu Aug 19 15:22:12 1999 +0200
@@ -135,12 +135,12 @@
 * many properties of integer multiplication, division and remainder
 are now available;
 
-* An interface to the Stanford Validity Checker (SVC) is available
-through the tactic svc_tac.  Propositional tautologies and theorems of
-linear arithmetic are proved automatically.  Numeric variables may
-have types nat, int or real.  SVC must be installed separately, and
-its results must be TAKEN ON TRUST (Isabelle does not check the
-proofs, but tags any invocation of the underlying oracle).
+* An interface to the Stanford Validity Checker (SVC) is available through the
+tactic svc_tac.  Propositional tautologies and theorems of linear arithmetic
+are proved automatically.  SVC must be installed separately, and its results
+must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any
+invocation of the underlying oracle).  For SVC see
+  http://agamemnon.stanford.edu/~levitt/vc/index.html
 
 * IsaMakefile: the HOL-Real target now builds an actual image;
 
@@ -160,8 +160,13 @@
 * HOL/typedef: fixed type inference for representing set; type
 arguments now have to occur explicitly on the rhs as type constraints;
 
-* HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects
-comma separated list of theorem names rather than an ML expression;
+* HOL/recdef (TFL): 'congs' syntax now expects comma separated list of theorem
+names rather than an ML expression;
+
+* HOL/defer_recdef (TFL): like recdef but the well-founded relation can be
+supplied later.  Program schemes can be defined, such as
+    "While B C s = (if B s then While B C (C s) else s)"
+where the well-founded relation can be chosen after B and C have been given.
 
 * HOL/List: the constructors of type list are now Nil and Cons;
 INCOMPATIBILITY: while [] and infix # syntax is still there, of