misc tuning for release;
authorwenzelm
Wed Oct 02 16:56:02 2013 +0200 (2013-10-02)
changeset 5403267ed9e57dd03
parent 54031 a3281fbe6856
child 54033 955c6549b3cb
misc tuning for release;
NEWS
     1.1 --- a/NEWS	Wed Oct 02 16:29:41 2013 +0200
     1.2 +++ b/NEWS	Wed Oct 02 16:56:02 2013 +0200
     1.3 @@ -136,12 +136,18 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* Improved support for ad hoc overloading of constants (see also
     1.8 -isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
     1.9 -
    1.10 -* Attibute 'code': 'code' now declares concrete and abstract code
    1.11 -equations uniformly.  Use explicit 'code equation' and 'code abstract'
    1.12 -to distinguish both when desired.
    1.13 +* Stronger precedence of syntax for big intersection and union on
    1.14 +sets, in accordance with corresponding lattice operations.
    1.15 +INCOMPATIBILITY.
    1.16 +
    1.17 +* Notation "{p:A. P}" now allows tuple patterns as well.
    1.18 +
    1.19 +* Nested case expressions are now translated in a separate check phase
    1.20 +rather than during parsing. The data for case combinators is separated
    1.21 +from the datatype package. The declaration attribute
    1.22 +"case_translation" can be used to register new case combinators:
    1.23 +
    1.24 +  declare [[case_translation case_combinator constructor1 ... constructorN]]
    1.25  
    1.26  * Code generator:
    1.27    - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' /
    1.28 @@ -152,23 +158,33 @@
    1.29  See the isar-ref manual for syntax diagrams, and the HOL theories for
    1.30  examples.
    1.31  
    1.32 -* HOL/BNF:
    1.33 -  - Various improvements to BNF-based (co)datatype package, including new
    1.34 -    commands "primrec_new", "primcorec", and "datatype_new_compat",
    1.35 -    as well as documentation. See "datatypes.pdf" for details.
    1.36 -  - New "coinduction" method to avoid some boilerplate (compared to coinduct).
    1.37 -  - Renamed keywords:
    1.38 -    data ~> datatype_new
    1.39 -    codata ~> codatatype
    1.40 -    bnf_def ~> bnf
    1.41 -  - Renamed many generated theorems, including
    1.42 -    discs ~> disc
    1.43 -    map_comp' ~> map_comp
    1.44 -    map_id' ~> map_id
    1.45 -    sels ~> sel
    1.46 -    set_map' ~> set_map
    1.47 -    sets ~> set
    1.48 -IMCOMPATIBILITY.
    1.49 +* Attibute 'code': 'code' now declares concrete and abstract code
    1.50 +equations uniformly.  Use explicit 'code equation' and 'code abstract'
    1.51 +to distinguish both when desired.
    1.52 +
    1.53 +* Discontinued theories Code_Integer and Efficient_Nat by a more
    1.54 +fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
    1.55 +Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
    1.56 +generation for details.  INCOMPATIBILITY.
    1.57 +
    1.58 +* Numeric types are mapped by default to target language numerals:
    1.59 +natural (replaces former code_numeral) and integer (replaces former
    1.60 +code_int).  Conversions are available as integer_of_natural /
    1.61 +natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
    1.62 +Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in
    1.63 +ML).  INCOMPATIBILITY.
    1.64 +
    1.65 +* Function package: For mutually recursive functions f and g, separate
    1.66 +cases rules f.cases and g.cases are generated instead of unusable
    1.67 +f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
    1.68 +in the case that the unusable rule was used nevertheless.
    1.69 +
    1.70 +* Function package: For each function f, new rules f.elims are
    1.71 +generated, which eliminate equalities of the form "f x = t".
    1.72 +
    1.73 +* New command 'fun_cases' derives ad-hoc elimination rules for
    1.74 +function equations as simplified instances of f.elims, analogous to
    1.75 +inductive_cases.  See ~~/src/HOL/ex/Fundefs.thy for some examples.
    1.76  
    1.77  * Lifting:
    1.78    - parametrized correspondence relations are now supported:
    1.79 @@ -200,35 +216,6 @@
    1.80    - Experimental support for transferring from the raw level to the
    1.81      abstract level: Transfer.transferred attribute
    1.82    - Attribute version of the transfer method: untransferred attribute
    1.83 -  
    1.84 -
    1.85 -* Function package: For mutually recursive functions f and g, separate
    1.86 -cases rules f.cases and g.cases are generated instead of unusable
    1.87 -f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY,
    1.88 -in the case that the unusable rule was used nevertheless.
    1.89 -
    1.90 -* Function package: For each function f, new rules f.elims are
    1.91 -automatically generated, which eliminate equalities of the form "f x =
    1.92 -t".
    1.93 -
    1.94 -* New command 'fun_cases' derives ad-hoc elimination rules for
    1.95 -function equations as simplified instances of f.elims, analogous to
    1.96 -inductive_cases.  See ~~/src/HOL/ex/Fundefs.thy for some examples.
    1.97 -
    1.98 -* Library/Polynomial.thy:
    1.99 -  - Use lifting for primitive definitions.
   1.100 -  - Explicit conversions from and to lists of coefficients, used for
   1.101 -    generated code.
   1.102 -  - Replaced recursion operator poly_rec by fold_coeffs.
   1.103 -  - Prefer pre-existing gcd operation for gcd.
   1.104 -  - Fact renames:
   1.105 -    poly_eq_iff ~> poly_eq_poly_eq_iff
   1.106 -    poly_ext ~> poly_eqI
   1.107 -    expand_poly_eq ~> poly_eq_iff
   1.108 -IMCOMPATIBILITY.
   1.109 -
   1.110 -* New Library/FSet.thy: type of finite sets defined as a subtype of
   1.111 -  sets defined by Lifting/Transfer
   1.112  
   1.113  * Reification and reflection:
   1.114    - Reification is now directly available in HOL-Main in structure
   1.115 @@ -237,24 +224,6 @@
   1.116    - The whole reflection stack has been decomposed into conversions.
   1.117  INCOMPATIBILITY.
   1.118  
   1.119 -* Stronger precedence of syntax for big intersection and union on
   1.120 -sets, in accordance with corresponding lattice operations.
   1.121 -INCOMPATIBILITY.
   1.122 -
   1.123 -* Nested case expressions are now translated in a separate check phase
   1.124 -rather than during parsing. The data for case combinators is separated
   1.125 -from the datatype package. The declaration attribute
   1.126 -"case_translation" can be used to register new case combinators:
   1.127 -
   1.128 -  declare [[case_translation case_combinator constructor1 ... constructorN]]
   1.129 -
   1.130 -* New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and
   1.131 -case_of_simps to convert function definitions between a list of
   1.132 -equations with patterns on the lhs and a single equation with case
   1.133 -expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.
   1.134 -
   1.135 -* Notation "{p:A. P}" now allows tuple patterns as well.
   1.136 -
   1.137  * Revised devices for recursive definitions over finite sets:
   1.138    - Only one fundamental fold combinator on finite set remains:
   1.139      Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b
   1.140 @@ -278,20 +247,6 @@
   1.141  
   1.142  * Locale hierarchy for abstract orderings and (semi)lattices.
   1.143  
   1.144 -* Discontinued theory src/HOL/Library/Eval_Witness.  INCOMPATIBILITY.
   1.145 -
   1.146 -* Numeric types mapped by default to target language numerals: natural
   1.147 -(replaces former code_numeral) and integer (replaces former code_int).
   1.148 -Conversions are available as integer_of_natural / natural_of_integer /
   1.149 -integer_of_nat / nat_of_integer (in HOL) and
   1.150 -Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in
   1.151 -ML).  INCOMPATIBILITY.
   1.152 -
   1.153 -* Discontinued theories Code_Integer and Efficient_Nat by a more
   1.154 -fine-grain stack of theories Code_Target_Int, Code_Binary_Nat,
   1.155 -Code_Target_Nat and Code_Target_Numeral.  See the tutorial on code
   1.156 -generation for details.  INCOMPATIBILITY.
   1.157 -
   1.158  * Complete_Partial_Order.admissible is defined outside the type class
   1.159  ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the
   1.160  class predicate assumption or sort constraint when possible.
   1.161 @@ -387,13 +342,6 @@
   1.162  
   1.163  INCOMPATIBILITY.
   1.164  
   1.165 -* Consolidation of library theories on product orders:
   1.166 -
   1.167 -    Product_Lattice ~> Product_Order -- pointwise order on products
   1.168 -    Product_ord ~> Product_Lexorder -- lexicographic order on products
   1.169 -
   1.170 -INCOMPATIBILITY.
   1.171 -
   1.172  * Nitpick:
   1.173    - Added option "spy"
   1.174    - Reduce incidence of "too high arity" errors
   1.175 @@ -406,6 +354,38 @@
   1.176    - Better support for "isar_proofs"
   1.177    - MaSh has been fined-tuned and now runs as a local server
   1.178  
   1.179 +* Improved support for ad hoc overloading of constants (see also
   1.180 +isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).
   1.181 +
   1.182 +* Library/Polynomial.thy:
   1.183 +  - Use lifting for primitive definitions.
   1.184 +  - Explicit conversions from and to lists of coefficients, used for
   1.185 +    generated code.
   1.186 +  - Replaced recursion operator poly_rec by fold_coeffs.
   1.187 +  - Prefer pre-existing gcd operation for gcd.
   1.188 +  - Fact renames:
   1.189 +    poly_eq_iff ~> poly_eq_poly_eq_iff
   1.190 +    poly_ext ~> poly_eqI
   1.191 +    expand_poly_eq ~> poly_eq_iff
   1.192 +IMCOMPATIBILITY.
   1.193 +
   1.194 +* New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and
   1.195 +case_of_simps to convert function definitions between a list of
   1.196 +equations with patterns on the lhs and a single equation with case
   1.197 +expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy.
   1.198 +
   1.199 +* New Library/FSet.thy: type of finite sets defined as a subtype of
   1.200 +sets defined by Lifting/Transfer.
   1.201 +
   1.202 +* Discontinued theory src/HOL/Library/Eval_Witness.  INCOMPATIBILITY.
   1.203 +
   1.204 +* Consolidation of library theories on product orders:
   1.205 +
   1.206 +    Product_Lattice ~> Product_Order -- pointwise order on products
   1.207 +    Product_ord ~> Product_Lexorder -- lexicographic order on products
   1.208 +
   1.209 +INCOMPATIBILITY.
   1.210 +
   1.211  * Imperative-HOL: The MREC combinator is considered legacy and no
   1.212  longer included by default. INCOMPATIBILITY, use partial_function
   1.213  instead, or import theory Legacy_Mrec as a fallback.
   1.214 @@ -415,6 +395,26 @@
   1.215  ~~/src/HOL/Library/Polynomial instead.  The latter provides
   1.216  integration with HOL's type classes for rings.  INCOMPATIBILITY.
   1.217  
   1.218 +* HOL/BNF:
   1.219 +  - Various improvements to BNF-based (co)datatype package, including
   1.220 +    new commands "primrec_new", "primcorec", and
   1.221 +    "datatype_new_compat", as well as documentation. See
   1.222 +    "datatypes.pdf" for details.
   1.223 +  - New "coinduction" method to avoid some boilerplate (compared to
   1.224 +    coinduct).
   1.225 +  - Renamed keywords:
   1.226 +    data ~> datatype_new
   1.227 +    codata ~> codatatype
   1.228 +    bnf_def ~> bnf
   1.229 +  - Renamed many generated theorems, including
   1.230 +    discs ~> disc
   1.231 +    map_comp' ~> map_comp
   1.232 +    map_id' ~> map_id
   1.233 +    sels ~> sel
   1.234 +    set_map' ~> set_map
   1.235 +    sets ~> set
   1.236 +IMCOMPATIBILITY.
   1.237 +
   1.238  
   1.239  *** ML ***
   1.240