1.1 --- a/NEWS Tue May 08 15:37:27 2007 +0200
1.2 +++ b/NEWS Tue May 08 17:40:18 2007 +0200
1.3 @@ -19,8 +19,9 @@
1.4 with Isar theories; migration is usually quite simple with the ML
1.5 function use_legacy_bindings. INCOMPATIBILITY.
1.6
1.7 -* Theory syntax: some popular names (e.g. "class", "fun", "help",
1.8 -"if") are now keywords. INCOMPATIBILITY, use double quotes.
1.9 +* Theory syntax: some popular names (e.g. 'class', 'declaration',
1.10 +'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double
1.11 +quotes.
1.12
1.13 * Legacy goal package: reduced interface to the bare minimum required
1.14 to keep existing proof scripts running. Most other user-level