author | wenzelm |

Wed Oct 02 16:56:02 2013 +0200 (2013-10-02) | |

changeset 54032 | 67ed9e57dd03 |

parent 54031 | a3281fbe6856 |

child 54033 | 955c6549b3cb |

misc tuning for release;

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