--- a/NEWS Tue Jun 10 15:30:06 2008 +0200
+++ b/NEWS Tue Jun 10 15:30:33 2008 +0200
@@ -1,6 +1,41 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+New
+---
+
+*** Pure ***
+
+* 'instance': attached definitions now longer accepted. INCOMPATIBILITY.
+
+* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY.
+
+
+*** HOL ***
+
+* 'rep_datatype': instead of theorem names the command now takes a list of terms
+denoting the constructors of the type to be represented as datatype. The
+characteristic theorems have to be proven. INCOMPATIBILITY. Also observe that
+the following theorems have disappeared in favour of existing ones:
+ unit_induct ~> unit.induct
+ prod_induct ~> prod.induct
+ sum_induct ~> sum.induct
+ Suc_Suc_eq ~> nat.inject
+ Suc_not_Zero Zero_not_Suc ~> nat.distinct
+
+* Tactics induct_tac and thm_induct_tac now take explicit context as arguments;
+type-specific induction rules are identified by the 'induct' attribute rather
+than querying the datatype package directly. INCOMPATIBILITY.
+
+* 'Least' operator now restricted to class 'order' (and subclasses).
+INCOMPATIBILITY.
+
+* Library/Nat_Infinity: added addition, numeral syntax and more instantiations
+for algebraic structures. Removed some duplicate theorems. Changes in simp
+rules. INCOMPATIBILITY.
+
+
+
New in Isabelle2008 (June 2008)
-------------------------------
@@ -150,7 +185,7 @@
reconstruction_modulus, reconstruction_sorts renamed
sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY.
-* Method "induction_scheme" derives user-specified induction rules
+* Method "induct_scheme" derives user-specified induction rules
from well-founded induction and completeness of patterns. This factors
out some operations that are done internally by the function package
and makes them available separately. See