changeset 25772 | 940429bb0743 |
parent 25737 | 84c92fc48e36 |
child 25776 | 4e4eb0f87850 |
--- a/NEWS Wed Jan 02 15:14:27 2008 +0100 +++ b/NEWS Wed Jan 02 15:39:42 2008 +0100 @@ -25,6 +25,9 @@ *** HOL *** +* New class "uminus" with operation "uminus" (split of from class "minus" +which now only has operation "minus", binary). + * New primrec package. Specification syntax conforms in style to definition/function/.... No separate induction rule is provided. The "primrec" command distinguishes old-style and new-style specifications