# HG changeset patch
# User paulson
# Date 864642894 -7200
# Node ID b99d750f6a3727f705182936f6c893c7d8bf4e04
# Parent  c056d328aa0ece1f487ef2495eb92a22cf937d71
Added recdef

diff -r c056d328aa0e -r b99d750f6a37 NEWS
--- a/NEWS	Mon May 26 12:34:05 1997 +0200
+++ b/NEWS	Mon May 26 12:34:54 1997 +0200
@@ -104,6 +104,9 @@
 
 * primrec now also works with type nat;
 
+* recdef: a new declaration form, allows general recursive functions to be
+defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
+
 * the constant for negation has been renamed from "not" to "Not" to
 harmonize with FOL, ZF, LK, etc.;