NEWS
changeset 40621 86f598f84188
parent 40580 0592d3a39c08
child 40624 2df58ba31be7
     1.1 --- a/NEWS	Wed Nov 17 11:39:44 2010 -0800
     1.2 +++ b/NEWS	Wed Nov 17 12:19:19 2010 -0800
     1.3 @@ -361,6 +361,121 @@
     1.4  * Removed [split_format ... and ... and ...] version of
     1.5  [split_format].  Potential INCOMPATIBILITY.
     1.6  
     1.7 +
     1.8 +*** HOLCF ***
     1.9 +
    1.10 +* The domain package now runs in definitional mode by default: The
    1.11 +former command 'new_domain' is now called 'domain'. To use the domain
    1.12 +package in its original axiomatic mode, use 'domain (unsafe)'.
    1.13 +INCOMPATIBILITY.
    1.14 +
    1.15 +* The new class 'domain' is now the default sort; the definitional
    1.16 +domain package and the powerdomain theories both require this class.
    1.17 +The new class 'predomain' is an unpointed version of 'domain'.
    1.18 +Theories can be updated by replacing sort annotations as shown below.
    1.19 +INCOMPATIBILITY.
    1.20 +
    1.21 +  'a::type ~> 'a::countable
    1.22 +  'a::cpo  ~> 'a::predomain
    1.23 +  'a::pcpo ~> 'a::domain
    1.24 +
    1.25 +* The old type class 'rep' has been superseded by class 'domain'.
    1.26 +Accordingly, users of the definitional package must remove any
    1.27 +'default_sort rep' declarations. INCOMPATIBILITY.
    1.28 +
    1.29 +* The old type classes 'profinite' and 'bifinite', along with the
    1.30 +overloaded constant 'approx' have been removed. INCOMPATIBILITY.
    1.31 +
    1.32 +* The type 'udom alg_defl' has been replaced by the non-parameterized
    1.33 +type 'defl'. HOLCF no longer defines an embedding of type defl into
    1.34 +udom by default; the instance proof defl :: domain is now available in
    1.35 +HOLCF/Library/Defl_Bifinite.thy.
    1.36 +
    1.37 +* The syntax 'REP('a)' has been replaced with 'DEFL('a)'.
    1.38 +
    1.39 +* The predicate 'directed' has been removed. INCOMPATIBILITY.
    1.40 +
    1.41 +* The type class 'finite_po' has been removed. INCOMPATIBILITY.
    1.42 +
    1.43 +* Renamed some theorems (the original names are also still available).
    1.44 +  expand_fun_below   ~> fun_below_iff
    1.45 +  below_fun_ext      ~> fun_belowI
    1.46 +  expand_cfun_eq     ~> cfun_eq_iff
    1.47 +  ext_cfun           ~> cfun_eqI
    1.48 +  expand_cfun_below  ~> cfun_below_iff
    1.49 +  below_cfun_ext     ~> cfun_belowI
    1.50 +  cont2cont_Rep_CFun ~> cont2cont_APP
    1.51 +
    1.52 +* The Abs and Rep functions for various types have changed names.
    1.53 +Related theorem names have also changed to match. INCOMPATIBILITY. 
    1.54 +  Rep_CFun  ~> Rep_cfun
    1.55 +  Abs_CFun  ~> Abs_cfun
    1.56 +  Rep_Sprod ~> Rep_sprod
    1.57 +  Abs_Sprod ~> Abs_sprod
    1.58 +  Rep_Ssum  ~> Rep_ssum
    1.59 +  Abs_Ssum  ~> Abs_ssum
    1.60 +
    1.61 +* Lemmas with names of the form *_defined_iff or *_strict_iff have
    1.62 +been renamed to *_bottom_iff. INCOMPATIBILITY.
    1.63 +
    1.64 +* Various changes to bisimulation/coinduction with domain package:
    1.65 +  - Definitions of 'bisim' constants no longer mention definedness.
    1.66 +  - With mutual recursion, 'bisim' predicate is now curried.
    1.67 +  - With mutual recursion, each type gets a separate coind theorem.
    1.68 +  - Variable names in bisim_def and coinduct rules have changed.
    1.69 +INCOMPATIBILITY.
    1.70 +
    1.71 +* Case combinators generated by the domain package for type 'foo'
    1.72 +are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
    1.73 +
    1.74 +* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
    1.75 +  sq_ord_less_eq_trans ~> below_eq_trans
    1.76 +  sq_ord_eq_less_trans ~> eq_below_trans
    1.77 +  refl_less            ~> below_refl
    1.78 +  trans_less           ~> below_trans
    1.79 +  antisym_less         ~> below_antisym
    1.80 +  antisym_less_inverse ~> po_eq_conv [THEN iffD1]
    1.81 +  box_less             ~> box_below
    1.82 +  rev_trans_less       ~> rev_below_trans
    1.83 +  not_less2not_eq      ~> not_below2not_eq
    1.84 +  less_UU_iff          ~> below_UU_iff
    1.85 +  flat_less_iff        ~> flat_below_iff
    1.86 +  adm_less             ~> adm_below
    1.87 +  adm_not_less         ~> adm_not_below
    1.88 +  adm_compact_not_less ~> adm_compact_not_below
    1.89 +  less_fun_def         ~> below_fun_def
    1.90 +  expand_fun_less      ~> fun_below_iff
    1.91 +  less_fun_ext         ~> fun_belowI
    1.92 +  less_discr_def       ~> below_discr_def
    1.93 +  discr_less_eq        ~> discr_below_eq
    1.94 +  less_unit_def        ~> below_unit_def
    1.95 +  less_cprod_def       ~> below_prod_def
    1.96 +  prod_lessI           ~> prod_belowI
    1.97 +  Pair_less_iff        ~> Pair_below_iff
    1.98 +  fst_less_iff         ~> fst_below_iff
    1.99 +  snd_less_iff         ~> snd_below_iff
   1.100 +  expand_cfun_less     ~> cfun_below_iff
   1.101 +  less_cfun_ext        ~> cfun_belowI
   1.102 +  injection_less       ~> injection_below
   1.103 +  less_up_def          ~> below_up_def
   1.104 +  not_Iup_less         ~> not_Iup_below
   1.105 +  Iup_less             ~> Iup_below
   1.106 +  up_less              ~> up_below
   1.107 +  Def_inject_less_eq   ~> Def_below_Def
   1.108 +  Def_less_is_eq       ~> Def_below_iff
   1.109 +  spair_less_iff       ~> spair_below_iff
   1.110 +  less_sprod           ~> below_sprod
   1.111 +  spair_less           ~> spair_below
   1.112 +  sfst_less_iff        ~> sfst_below_iff
   1.113 +  ssnd_less_iff        ~> ssnd_below_iff
   1.114 +  fix_least_less       ~> fix_least_below
   1.115 +  dist_less_one        ~> dist_below_one
   1.116 +  less_ONE             ~> below_ONE
   1.117 +  ONE_less_iff         ~> ONE_below_iff
   1.118 +  less_sinlD           ~> below_sinlD
   1.119 +  less_sinrD           ~> below_sinrD
   1.120 +
   1.121 +
   1.122  *** FOL ***
   1.123  
   1.124  * All constant names are now qualified.  INCOMPATIBILITY.