--- 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 --