some tuning for release;
authorwenzelm
Wed Sep 07 20:29:54 2011 +0200 (2011-09-07)
changeset 448000472f2367efb
parent 44799 1fd0a1276a09
child 44801 a0459c50cfc9
child 44810 c1c05a578c1a
some tuning for release;
NEWS
     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)