NEWS
changeset 3338 b99d750f6a37
parent 3321 c609a0119fd8
child 3454 40b1287347d7
     1.1 --- a/NEWS	Mon May 26 12:34:05 1997 +0200
     1.2 +++ b/NEWS	Mon May 26 12:34:54 1997 +0200
     1.3 @@ -104,6 +104,9 @@
     1.4  
     1.5  * primrec now also works with type nat;
     1.6  
     1.7 +* recdef: a new declaration form, allows general recursive functions to be
     1.8 +defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
     1.9 +
    1.10  * the constant for negation has been renamed from "not" to "Not" to
    1.11  harmonize with FOL, ZF, LK, etc.;
    1.12