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