--- a/NEWS Wed Nov 17 11:39:44 2010 -0800
+++ b/NEWS Wed Nov 17 12:19:19 2010 -0800
@@ -361,6 +361,121 @@
* Removed [split_format ... and ... and ...] version of
[split_format]. Potential INCOMPATIBILITY.
+
+*** HOLCF ***
+
+* The domain package now runs in definitional mode by default: The
+former command 'new_domain' is now called 'domain'. To use the domain
+package in its original axiomatic mode, use 'domain (unsafe)'.
+INCOMPATIBILITY.
+
+* The new class 'domain' is now the default sort; the definitional
+domain package and the powerdomain theories both require this class.
+The new class 'predomain' is an unpointed version of 'domain'.
+Theories can be updated by replacing sort annotations as shown below.
+INCOMPATIBILITY.
+
+ 'a::type ~> 'a::countable
+ 'a::cpo ~> 'a::predomain
+ 'a::pcpo ~> 'a::domain
+
+* The old type class 'rep' has been superseded by class 'domain'.
+Accordingly, users of the definitional package must remove any
+'default_sort rep' declarations. INCOMPATIBILITY.
+
+* The old type classes 'profinite' and 'bifinite', along with the
+overloaded constant 'approx' have been removed. INCOMPATIBILITY.
+
+* The type 'udom alg_defl' has been replaced by the non-parameterized
+type 'defl'. HOLCF no longer defines an embedding of type defl into
+udom by default; the instance proof defl :: domain is now available in
+HOLCF/Library/Defl_Bifinite.thy.
+
+* The syntax 'REP('a)' has been replaced with 'DEFL('a)'.
+
+* The predicate 'directed' has been removed. INCOMPATIBILITY.
+
+* The type class 'finite_po' has been removed. INCOMPATIBILITY.
+
+* Renamed some theorems (the original names are also still available).
+ expand_fun_below ~> fun_below_iff
+ below_fun_ext ~> fun_belowI
+ expand_cfun_eq ~> cfun_eq_iff
+ ext_cfun ~> cfun_eqI
+ expand_cfun_below ~> cfun_below_iff
+ below_cfun_ext ~> cfun_belowI
+ cont2cont_Rep_CFun ~> cont2cont_APP
+
+* The Abs and Rep functions for various types have changed names.
+Related theorem names have also changed to match. INCOMPATIBILITY.
+ Rep_CFun ~> Rep_cfun
+ Abs_CFun ~> Abs_cfun
+ Rep_Sprod ~> Rep_sprod
+ Abs_Sprod ~> Abs_sprod
+ Rep_Ssum ~> Rep_ssum
+ Abs_Ssum ~> Abs_ssum
+
+* Lemmas with names of the form *_defined_iff or *_strict_iff have
+been renamed to *_bottom_iff. INCOMPATIBILITY.
+
+* Various changes to bisimulation/coinduction with domain package:
+ - Definitions of 'bisim' constants no longer mention definedness.
+ - With mutual recursion, 'bisim' predicate is now curried.
+ - With mutual recursion, each type gets a separate coind theorem.
+ - Variable names in bisim_def and coinduct rules have changed.
+INCOMPATIBILITY.
+
+* Case combinators generated by the domain package for type 'foo'
+are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
+
+* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
+ sq_ord_less_eq_trans ~> below_eq_trans
+ sq_ord_eq_less_trans ~> eq_below_trans
+ refl_less ~> below_refl
+ trans_less ~> below_trans
+ antisym_less ~> below_antisym
+ antisym_less_inverse ~> po_eq_conv [THEN iffD1]
+ box_less ~> box_below
+ rev_trans_less ~> rev_below_trans
+ not_less2not_eq ~> not_below2not_eq
+ less_UU_iff ~> below_UU_iff
+ flat_less_iff ~> flat_below_iff
+ adm_less ~> adm_below
+ adm_not_less ~> adm_not_below
+ adm_compact_not_less ~> adm_compact_not_below
+ less_fun_def ~> below_fun_def
+ expand_fun_less ~> fun_below_iff
+ less_fun_ext ~> fun_belowI
+ less_discr_def ~> below_discr_def
+ discr_less_eq ~> discr_below_eq
+ less_unit_def ~> below_unit_def
+ less_cprod_def ~> below_prod_def
+ prod_lessI ~> prod_belowI
+ Pair_less_iff ~> Pair_below_iff
+ fst_less_iff ~> fst_below_iff
+ snd_less_iff ~> snd_below_iff
+ expand_cfun_less ~> cfun_below_iff
+ less_cfun_ext ~> cfun_belowI
+ injection_less ~> injection_below
+ less_up_def ~> below_up_def
+ not_Iup_less ~> not_Iup_below
+ Iup_less ~> Iup_below
+ up_less ~> up_below
+ Def_inject_less_eq ~> Def_below_Def
+ Def_less_is_eq ~> Def_below_iff
+ spair_less_iff ~> spair_below_iff
+ less_sprod ~> below_sprod
+ spair_less ~> spair_below
+ sfst_less_iff ~> sfst_below_iff
+ ssnd_less_iff ~> ssnd_below_iff
+ fix_least_less ~> fix_least_below
+ dist_less_one ~> dist_below_one
+ less_ONE ~> below_ONE
+ ONE_less_iff ~> ONE_below_iff
+ less_sinlD ~> below_sinlD
+ less_sinrD ~> below_sinrD
+
+
*** FOL ***
* All constant names are now qualified. INCOMPATIBILITY.