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