1.1 --- a/NEWS	Tue May 11 11:02:56 2010 -0700
     1.2 +++ b/NEWS	Tue May 11 11:40:39 2010 -0700
     1.3 @@ -320,6 +320,58 @@
     1.4    Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
     1.5  
     1.6  
     1.7 +*** HOLCF ***
     1.8 +
     1.9 +* Variable names in lemmas generated by the domain package have
    1.10 +changed; the naming scheme is now consistent with the HOL datatype
    1.11 +package.  Some proof scripts may be affected, INCOMPATIBILITY.
    1.12 +
    1.13 +* The domain package no longer defines the function "foo_copy" for
    1.14 +recursive domain "foo".  The reach lemma is now stated directly in
    1.15 +terms of "foo_take".  Lemmas and proofs that mention "foo_copy" must
    1.16 +be reformulated in terms of "foo_take", INCOMPATIBILITY.
    1.17 +
    1.18 +* Most definedness lemmas generated by the domain package (previously
    1.19 +of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form
    1.20 +like "foo$x = UU <-> x = UU", which works better as a simp rule.
    1.21 +Proof scripts that used definedness lemmas as intro rules may break,
    1.22 +potential INCOMPATIBILITY.
    1.23 +
    1.24 +* Induction and casedist rules generated by the domain package now
    1.25 +declare proper case_names (one called "bottom", and one named for each
    1.26 +constructor).  INCOMPATIBILITY.
    1.27 +
    1.28 +* For mutually-recursive domains, separate "reach" and "take_lemma"
    1.29 +rules are generated for each domain, INCOMPATIBILITY.
    1.30 +
    1.31 +  foo_bar.reach       ~> foo.reach  bar.reach
    1.32 +  foo_bar.take_lemmas ~> foo.take_lemma  bar.take_lemma
    1.33 +
    1.34 +* Some lemmas generated by the domain package have been renamed for
    1.35 +consistency with the datatype package, INCOMPATIBILITY.
    1.36 +
    1.37 +  foo.ind        ~> foo.induct
    1.38 +  foo.finite_ind ~> foo.finite_induct
    1.39 +  foo.coind      ~> foo.coinduct
    1.40 +  foo.casedist   ~> foo.exhaust
    1.41 +  foo.exhaust    ~> foo.nchotomy
    1.42 +
    1.43 +* For consistency with other definition packages, the fixrec package
    1.44 +now generates qualified theorem names, INCOMPATIBILITY.
    1.45 +
    1.46 +  foo_simps  ~> foo.simps
    1.47 +  foo_unfold ~> foo.unfold
    1.48 +  foo_induct ~> foo.induct
    1.49 +
    1.50 +* The "contlub" predicate has been removed.  Proof scripts should use
    1.51 +lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY.
    1.52 +
    1.53 +* The "admw" predicate has been removed, INCOMPATIBILITY.
    1.54 +
    1.55 +* The constants cpair, cfst, and csnd have been removed in favor of
    1.56 +Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY.
    1.57 +
    1.58 +
    1.59  *** ML ***
    1.60  
    1.61  * Sorts.certify_sort and derived "cert" operations for types and terms