author | paulson |
Mon, 26 May 1997 12:34:54 +0200 | |
changeset 3338 | b99d750f6a37 |
parent 3337 | c056d328aa0e |
child 3339 | cfa72a70f2b5 |
--- 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.;