author | wenzelm |

Wed Sep 07 20:29:54 2011 +0200 (2011-09-07) | |

changeset 44800 | 0472f2367efb |

parent 44799 | 1fd0a1276a09 |

child 44801 | a0459c50cfc9 |

child 44810 | c1c05a578c1a |

some tuning for release;

1.1 --- a/NEWS Wed Sep 07 18:01:01 2011 +0200 1.2 +++ b/NEWS Wed Sep 07 20:29:54 2011 +0200 1.3 @@ -34,6 +34,13 @@ 1.4 See also ~~/src/Tools/jEdit/README.html for further information, 1.5 including some remaining limitations. 1.6 1.7 +* Theory loader: source files are exclusively located via the master 1.8 +directory of each theory node (where the .thy file itself resides). 1.9 +The global load path (such as src/HOL/Library) has been discontinued. 1.10 +Note that the path element ~~ may be used to reference theories in the 1.11 +Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet". 1.12 +INCOMPATIBILITY. 1.13 + 1.14 * Theory loader: source files are identified by content via SHA1 1.15 digests. Discontinued former path/modtime identification and optional 1.16 ISABELLE_FILE_IDENT plugin scripts. 1.17 @@ -48,13 +55,6 @@ 1.18 * Discontinued old lib/scripts/polyml-platform, which has been 1.19 obsolete since Isabelle2009-2. 1.20 1.21 -* Theory loader: source files are exclusively located via the master 1.22 -directory of each theory node (where the .thy file itself resides). 1.23 -The global load path (such as src/HOL/Library) has been discontinued. 1.24 -Note that the path element ~~ may be used to reference theories in the 1.25 -Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet". 1.26 -INCOMPATIBILITY. 1.27 - 1.28 * Various optional external tools are referenced more robustly and 1.29 uniformly by explicit Isabelle settings as follows: 1.30 1.31 @@ -82,29 +82,35 @@ 1.32 that the result needs to be unique, which means fact specifications 1.33 may have to be refined after enriching a proof context. 1.34 1.35 +* Attribute "case_names" has been refined: the assumptions in each case 1.36 +can be named now by following the case name with [name1 name2 ...]. 1.37 + 1.38 * Isabelle/Isar reference manual provides more formal references in 1.39 syntax diagrams. 1.40 1.41 -* Attribute case_names has been refined: the assumptions in each case can 1.42 -be named now by following the case name with [name1 name2 ...]. 1.43 - 1.44 1.45 *** HOL *** 1.46 1.47 -* Classes bot and top require underlying partial order rather than preorder: 1.48 -uniqueness of bot and top is guaranteed. INCOMPATIBILITY. 1.49 +* Classes bot and top require underlying partial order rather than 1.50 +preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. 1.51 1.52 * Class complete_lattice: generalized a couple of lemmas from sets; 1.53 -generalized theorems INF_cong and SUP_cong. New type classes for complete 1.54 -boolean algebras and complete linear orders. Lemmas Inf_less_iff, 1.55 -less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder. 1.56 -Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, Sup_fun_def, 1.57 -Inf_apply, Sup_apply. 1.58 +generalized theorems INF_cong and SUP_cong. New type classes for 1.59 +complete boolean algebras and complete linear orders. Lemmas 1.60 +Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in 1.61 +class complete_linorder. 1.62 + 1.63 +Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, 1.64 +Sup_fun_def, Inf_apply, Sup_apply. 1.65 + 1.66 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, 1.67 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, 1.68 -INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image, 1.69 -Union_def, UN_singleton, UN_eq have been discarded. 1.70 -More consistent and less misunderstandable names: 1.71 +INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, 1.72 +UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been 1.73 +discarded. 1.74 + 1.75 +More consistent and comprehensive names: 1.76 + 1.77 INFI_def ~> INF_def 1.78 SUPR_def ~> SUP_def 1.79 INF_leI ~> INF_lower 1.80 @@ -122,30 +128,35 @@ 1.81 1.82 INCOMPATIBILITY. 1.83 1.84 -* Theorem collections ball_simps and bex_simps do not contain theorems referring 1.85 -to UNION any longer; these have been moved to collection UN_ball_bex_simps. 1.86 -INCOMPATIBILITY. 1.87 - 1.88 -* Archimedean_Field.thy: 1.89 - floor now is defined as parameter of a separate type class floor_ceiling. 1.90 - 1.91 -* Finite_Set.thy: more coherent development of fold_set locales: 1.92 +* Theorem collections ball_simps and bex_simps do not contain theorems 1.93 +referring to UNION any longer; these have been moved to collection 1.94 +UN_ball_bex_simps. INCOMPATIBILITY. 1.95 + 1.96 +* Theory Archimedean_Field: floor now is defined as parameter of a 1.97 +separate type class floor_ceiling. 1.98 + 1.99 +* Theory Finite_Set: more coherent development of fold_set locales: 1.100 1.101 locale fun_left_comm ~> locale comp_fun_commute 1.102 locale fun_left_comm_idem ~> locale comp_fun_idem 1.103 - 1.104 -Both use point-free characterisation; interpretation proofs may need adjustment. 1.105 -INCOMPATIBILITY. 1.106 + 1.107 +Both use point-free characterization; interpretation proofs may need 1.108 +adjustment. INCOMPATIBILITY. 1.109 1.110 * Code generation: 1.111 - - theory Library/Code_Char_ord provides native ordering of characters 1.112 - in the target language. 1.113 - - commands code_module and code_library are legacy, use export_code instead. 1.114 - - method evaluation is legacy, use method eval instead. 1.115 - - legacy evaluator "SML" is deactivated by default. To activate it, add the following 1.116 - line in your theory: 1.117 + 1.118 + - Theory Library/Code_Char_ord provides native ordering of 1.119 + characters in the target language. 1.120 + 1.121 + - Commands code_module and code_library are legacy, use export_code instead. 1.122 + 1.123 + - Method "evaluation" is legacy, use method "eval" instead. 1.124 + 1.125 + - Legacy evaluator "SML" is deactivated by default. May be 1.126 + reactivated by the following theory command: 1.127 + 1.128 setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} 1.129 - 1.130 + 1.131 * Declare ext [intro] by default. Rare INCOMPATIBILITY. 1.132 1.133 * Nitpick: 1.134 @@ -168,51 +179,57 @@ 1.135 - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. 1.136 - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY. 1.137 1.138 -* "try": 1.139 - - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:" 1.140 - options. INCOMPATIBILITY. 1.141 - - Introduced "try" that not only runs "try_methods" but also "solve_direct", 1.142 - "sledgehammer", "quickcheck", and "nitpick". 1.143 +* Command 'try': 1.144 + - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and 1.145 + "elim:" options. INCOMPATIBILITY. 1.146 + - Introduced 'tryĆ that not only runs 'try_methods' but also 1.147 + 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. 1.148 1.149 * Quickcheck: 1.150 + 1.151 - Added "eval" option to evaluate terms for the found counterexample 1.152 - (currently only supported by the default (exhaustive) tester) 1.153 + (currently only supported by the default (exhaustive) tester). 1.154 + 1.155 - Added post-processing of terms to obtain readable counterexamples 1.156 - (currently only supported by the default (exhaustive) tester) 1.157 + (currently only supported by the default (exhaustive) tester). 1.158 + 1.159 - New counterexample generator quickcheck[narrowing] enables 1.160 - narrowing-based testing. 1.161 - It requires that the Glasgow Haskell compiler is installed and 1.162 - its location is known to Isabelle with the environment variable 1.163 - ISABELLE_GHC. 1.164 + narrowing-based testing. Requires the Glasgow Haskell compiler 1.165 + with its installation location defined in the Isabelle settings 1.166 + environment as ISABELLE_GHC. 1.167 + 1.168 - Removed quickcheck tester "SML" based on the SML code generator 1.169 - from HOL-Library 1.170 + (formly in HOL/Library). 1.171 1.172 * Function package: discontinued option "tailrec". 1.173 -INCOMPATIBILITY. Use partial_function instead. 1.174 - 1.175 -* HOL-Probability: 1.176 +INCOMPATIBILITY. Use 'partial_function' instead. 1.177 + 1.178 +* Session HOL-Probability: 1.179 - Caratheodory's extension lemma is now proved for ring_of_sets. 1.180 - Infinite products of probability measures are now available. 1.181 - - Use extended reals instead of positive extended reals. 1.182 - INCOMPATIBILITY. 1.183 - 1.184 -* Old recdef package has been moved to Library/Old_Recdef.thy, where it 1.185 -must be loaded explicitly. INCOMPATIBILITY. 1.186 - 1.187 -* Well-founded recursion combinator "wfrec" has been moved to 1.188 -Library/Wfrec.thy. INCOMPATIBILITY. 1.189 - 1.190 -* Theory Library/Nat_Infinity has been renamed to Library/Extended_Nat. 1.191 -The names of the following types and constants have changed: 1.192 - inat (type) ~> enat 1.193 + - Use extended reals instead of positive extended 1.194 + reals. INCOMPATIBILITY. 1.195 + 1.196 +* Old 'recdef' package has been moved to theory Library/Old_Recdef, 1.197 +from where it must be imported explicitly. INCOMPATIBILITY. 1.198 + 1.199 +* Well-founded recursion combinator "wfrec" has been moved to theory 1.200 +Library/Wfrec. INCOMPATIBILITY. 1.201 + 1.202 +* Theory Library/Nat_Infinity has been renamed to 1.203 +Library/Extended_Nat, with name changes of the following types and 1.204 +constants: 1.205 + 1.206 + type inat ~> type enat 1.207 Fin ~> enat 1.208 Infty ~> infinity (overloaded) 1.209 iSuc ~> eSuc 1.210 the_Fin ~> the_enat 1.211 + 1.212 Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has 1.213 been renamed accordingly. 1.214 1.215 -* Limits.thy: Type "'a net" has been renamed to "'a filter", in 1.216 +* Theory Limits: Type "'a net" has been renamed to "'a filter", in 1.217 accordance with standard mathematical terminology. INCOMPATIBILITY. 1.218 1.219 * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed 1.220 @@ -283,10 +300,10 @@ 1.221 real_abs_sub_norm ~> norm_triangle_ineq3 1.222 norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 1.223 1.224 -* Complex_Main: The locale interpretations for the bounded_linear and 1.225 -bounded_bilinear locales have been removed, in order to reduce the 1.226 -number of duplicate lemmas. Users must use the original names for 1.227 -distributivity theorems, potential INCOMPATIBILITY. 1.228 +* Theory Complex_Main: The locale interpretations for the 1.229 +bounded_linear and bounded_bilinear locales have been removed, in 1.230 +order to reduce the number of duplicate lemmas. Users must use the 1.231 +original names for distributivity theorems, potential INCOMPATIBILITY. 1.232 1.233 divide.add ~> add_divide_distrib 1.234 divide.diff ~> diff_divide_distrib 1.235 @@ -296,7 +313,7 @@ 1.236 mult_right.setsum ~> setsum_right_distrib 1.237 mult_left.diff ~> left_diff_distrib 1.238 1.239 -* Complex_Main: Several redundant theorems have been removed or 1.240 +* Theory Complex_Main: Several redundant theorems have been removed or 1.241 replaced by more general versions. INCOMPATIBILITY. 1.242 1.243 real_0_le_divide_iff ~> zero_le_divide_iff 1.244 @@ -364,26 +381,30 @@ 1.245 1.246 *** Document preparation *** 1.247 1.248 -* Discontinued special treatment of hard tabulators, which are better 1.249 -avoided in the first place. Implicit tab-width is 1. 1.250 - 1.251 -* Antiquotation @{rail} layouts railroad syntax diagrams, see also 1.252 -isar-ref manual. 1.253 - 1.254 -* Antiquotation @{value} evaluates the given term and presents its result. 1.255 - 1.256 * Localized \isabellestyle switch can be used within blocks or groups 1.257 like this: 1.258 1.259 \isabellestyle{it} %preferred default 1.260 {\isabellestylett @{text "typewriter stuff"}} 1.261 1.262 -* New term style "isub" as ad-hoc conversion of variables x1, y23 into 1.263 -subscripted form x\<^isub>1, y\<^isub>2\<^isub>3. 1.264 +* Antiquotation @{rail} layouts railroad syntax diagrams, see also 1.265 +isar-ref manual, both for description and actual application of the 1.266 +same. 1.267 + 1.268 +* Antiquotation @{value} evaluates the given term and presents its 1.269 +result. 1.270 + 1.271 +* Antiquotations: term style "isub" provides ad-hoc conversion of 1.272 +variables x1, y23 into subscripted form x\<^isub>1, 1.273 +y\<^isub>2\<^isub>3. 1.274 1.275 * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then> 1.276 (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). 1.277 1.278 +* Discontinued special treatment of hard tabulators, which are better 1.279 +avoided in the first place (no universally agreed standard expansion). 1.280 +Implicit tab-width is now 1. 1.281 + 1.282 1.283 *** ML *** 1.284 1.285 @@ -443,11 +464,14 @@ 1.286 proper Proof.context. 1.287 1.288 * Scala layer provides JVM method invocation service for static 1.289 -methods of type (String)String, see Invoke_Scala.method in ML. 1.290 -For example: 1.291 +methods of type (String)String, see Invoke_Scala.method in ML. For 1.292 +example: 1.293 1.294 Invoke_Scala.method "java.lang.System.getProperty" "java.home" 1.295 1.296 +Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this 1.297 +allows to pass structured values between ML and Scala. 1.298 + 1.299 1.300 1.301 New in Isabelle2011 (January 2011)