# HG changeset patch
# User huffman
# Date 1273603239 25200
# Node ID 6a47f043d498185a2ba6c8a6f45034bf69846127
# Parent  84ee370b4b1b208b12768c9b06097bd15e1317a2
collected NEWS updates for HOLCF

diff -r 84ee370b4b1b -r 6a47f043d498 NEWS
--- 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