changeset 25609 | b1950d5e13dc |
parent 25599 | afdff3ad4057 |
child 25626 | 3000965b1fdf |
--- a/NEWS Wed Dec 12 09:00:07 2007 +0100 +++ b/NEWS Wed Dec 12 19:26:37 2007 +0100 @@ -28,6 +28,8 @@ definition/function/.... No separate induction rule is provided. The "primrec" command distinguishes old-style and new-style specifications by syntax. The former primrec package is now named OldPrimrecPackage. +When adjusting theories, beware: constants stemming for new-style +primrec specifications have authentic syntax. * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.