* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
* Isar: schematic goals are no longer restricted to higher-order patterns.
* ML/Pure: Logic.(un)varify only works in a global context, which is now enforced.

--- a/NEWS	Wed Jun 07 02:01:36 2006 +0200
+++ b/NEWS	Wed Jun 07 02:04:20 2006 +0200
@@ -15,6 +15,9 @@
 with Isar theories; migration is usually quite simple with the ML
 function use_legacy_bindings.  INCOMPATIBILITY.
 
+* Theory syntax: some popular names (e.g. "class", "if") are now
+keywords.  INCOMPATIBILITY, use double quotes.
+
 * Legacy goal package: reduced interface to the bare minimum required
 to keep existing proof scripts running.  Most other user-level
 functions are now part of the OldGoals structure, which is *not* open
@@ -104,6 +107,10 @@
 simplifies all new goals that emerge from applying rule foo to the
 originally first one.
 
+* Isar: schematic goals are no longer restricted to higher-order
+patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as
+expected.
+
 * Isar: the conclusion of a long theorem statement is now either
 'shows' (a simultaneous conjunction, as before), or 'obtains'
 (essentially a disjunction of cases with local parameters and
@@ -524,6 +531,10 @@
 signature declarations.  (This information is not relevant to the
 logic, but only for type inference.)  IMPORTANT INTERNAL CHANGE.
 
+* Pure: Logic.(un)varify only works in a global context, which is now
+enforced instead of silently assumed.  INCOMPATIBILITY, may use
+Logic.legacy_(un)varify as temporary workaround.
+
 * Pure: axiomatic type classes are now purely definitional, with
 explicit proofs of class axioms and super class relations performed
 internally.  See Pure/axclass.ML for the main internal interfaces --