--- a/NEWS Tue Sep 02 18:01:24 2008 +0200
+++ b/NEWS Tue Sep 02 20:04:26 2008 +0200
@@ -46,9 +46,9 @@
*** HOL ***
-* HOL/Orderings: class "wellorder" moved here, with explicit induction rule
-"less_induct" as assumption. For instantiation of "wellorder" by means
-of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY.
+* HOL/Orderings: class "wellorder" moved here, with explicit induction
+rule "less_induct" as assumption. For instantiation of "wellorder" by
+means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY.
* HOL/Orderings: added class "preorder" as superclass of "order".
INCOMPATIBILITY: Instantiation proofs for order, linorder
@@ -138,7 +138,8 @@
instantiations for algebraic structures. Removed some duplicate
theorems. Changes in simp rules. INCOMPATIBILITY.
-* ATP selection (E/Vampire/Spass) is now via PG's settings menu.
+* ATP selection (E/Vampire/Spass) is now via Proof General's settings
+menu.
*** HOL-Algebra ***
@@ -178,7 +179,15 @@
*** ML ***
-
+
+* Name bindings in higher specification mechanisms (notably
+LocalTheory.define, LocalTheory.note, and derived packages) are now
+formalized as type Name.binding, replacing old bstring.
+INCOMPATIBILITY, need to wrap strings via Name.binding function, see
+also Name.name_of. Packages should pass name bindings given by the
+user to underlying specification mechanisms; this enables precise
+tracking of source positions, for example.
+
* Rules and tactics that read instantiations (read_instantiate,
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
context, which is required for parsing and type-checking. Moreover,