# HG changeset patch
# User huffman
# Date 1290025159 28800
# Node ID 86f598f84188680d3f50febde93de186463392d9
# Parent  7a9278de19ad5d83acaca48df52545576c15054a
accumulated NEWS updates for HOLCF

diff -r 7a9278de19ad -r 86f598f84188 NEWS
--- 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.