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)