--- a/NEWS Tue May 11 11:02:56 2010 -0700
+++ b/NEWS Tue May 11 11:40:39 2010 -0700
@@ -320,6 +320,58 @@
Nat_Int_Bij.bij_int_to_nat_bij ~> bij_int_decode
+*** HOLCF ***
+
+* Variable names in lemmas generated by the domain package have
+changed; the naming scheme is now consistent with the HOL datatype
+package. Some proof scripts may be affected, INCOMPATIBILITY.
+
+* The domain package no longer defines the function "foo_copy" for
+recursive domain "foo". The reach lemma is now stated directly in
+terms of "foo_take". Lemmas and proofs that mention "foo_copy" must
+be reformulated in terms of "foo_take", INCOMPATIBILITY.
+
+* Most definedness lemmas generated by the domain package (previously
+of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
+like "foo$x = UU <-> x = UU", which works better as a simp rule.
+Proof scripts that used definedness lemmas as intro rules may break,
+potential INCOMPATIBILITY.
+
+* Induction and casedist rules generated by the domain package now
+declare proper case_names (one called "bottom", and one named for each
+constructor). INCOMPATIBILITY.
+
+* For mutually-recursive domains, separate "reach" and "take_lemma"
+rules are generated for each domain, INCOMPATIBILITY.
+
+ foo_bar.reach ~> foo.reach bar.reach
+ foo_bar.take_lemmas ~> foo.take_lemma bar.take_lemma
+
+* Some lemmas generated by the domain package have been renamed for
+consistency with the datatype package, INCOMPATIBILITY.
+
+ foo.ind ~> foo.induct
+ foo.finite_ind ~> foo.finite_induct
+ foo.coind ~> foo.coinduct
+ foo.casedist ~> foo.exhaust
+ foo.exhaust ~> foo.nchotomy
+
+* For consistency with other definition packages, the fixrec package
+now generates qualified theorem names, INCOMPATIBILITY.
+
+ foo_simps ~> foo.simps
+ foo_unfold ~> foo.unfold
+ foo_induct ~> foo.induct
+
+* The "contlub" predicate has been removed. Proof scripts should use
+lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
+
+* The "admw" predicate has been removed, INCOMPATIBILITY.
+
+* The constants cpair, cfst, and csnd have been removed in favor of
+Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
+
+
*** ML ***
* Sorts.certify_sort and derived "cert" operations for types and terms