author | wenzelm |

Sun Sep 18 14:34:24 2011 +0200 (2011-09-18) | |

changeset 44967 | b94c1614e7d5 |

parent 44966 | 1db165e0bd97 |

child 44968 | 52744e144432 |

misc tuning for release;

1.1 --- a/CONTRIBUTORS Sun Sep 18 14:25:53 2011 +0200 1.2 +++ b/CONTRIBUTORS Sun Sep 18 14:34:24 2011 +0200 1.3 @@ -12,30 +12,30 @@ 1.4 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM 1.5 Refined theory on complete lattices. 1.6 1.7 +* August 2011: Brian Huffman, Portland State University 1.8 + Miscellaneous cleanup of Complex_Main and Multivariate_Analysis. 1.9 + 1.10 +* June 2011: Brian Huffman, Portland State University 1.11 + Proof method "countable_datatype" for theory Library/Countable. 1.12 + 1.13 +* 2011: Jasmin Blanchette, TUM 1.14 + Various improvements to Sledgehammer, notably: use of sound 1.15 + translations, support for more provers (Waldmeister, LEO-II, 1.16 + Satallax). Further development of Nitpick and 'try' command. 1.17 + 1.18 +* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology 1.19 + Theory HOL/Library/Cset_Monad allows do notation for computable sets 1.20 + (cset) via the generic monad ad-hoc overloading facility. 1.21 + 1.22 +* 2011: Johannes Hölzl, Armin Heller, TUM and 1.23 + Bogdan Grechuk, University of Edinburgh 1.24 + Theory HOL/Library/Extended_Reals: real numbers extended with plus 1.25 + and minus infinity. 1.26 + 1.27 * 2011: Makarius Wenzel, Université Paris-Sud / LRI 1.28 Various building blocks for Isabelle/Scala layer and Isabelle/jEdit 1.29 Prover IDE. 1.30 1.31 -* 2011: Jasmin Blanchette, TUM 1.32 - Various improvements to Sledgehammer, notably: use of sound translations, 1.33 - support for more provers (Waldmeister, LEO-II, Satallax). Further development 1.34 - of Nitpick and "try". 1.35 - 1.36 -* 2011: Andreas Lochbihler, Karlsruhe Institute of Technology 1.37 - Theory HOL/Library/Cset_Monad allows do notation for computable 1.38 - sets (cset) via the generic monad ad-hoc overloading facility. 1.39 - 1.40 -* 2011: Johannes Hölzl, Armin Heller, TUM, 1.41 - and Bogdan Grechuk, University of Edinburgh 1.42 - Theory HOL/Library/Extended_Reals: real numbers extended with 1.43 - plus and minus infinity. 1.44 - 1.45 -* June 2011: Brian Huffman, Portland State University 1.46 - Proof method 'countable_datatype' for theory Library/Countable. 1.47 - 1.48 -* August 2011: Brian Huffman, Portland State University 1.49 - Misc cleanup of Complex_Main and Multivariate_Analysis. 1.50 - 1.51 1.52 Contributions to Isabelle2011 1.53 -----------------------------

2.1 --- a/NEWS Sun Sep 18 14:25:53 2011 +0200 2.2 +++ b/NEWS Sun Sep 18 14:34:24 2011 +0200 2.3 @@ -55,18 +55,6 @@ 2.4 * Discontinued old lib/scripts/polyml-platform, which has been 2.5 obsolete since Isabelle2009-2. 2.6 2.7 -* Various optional external tools are referenced more robustly and 2.8 -uniformly by explicit Isabelle settings as follows: 2.9 - 2.10 - ISABELLE_CSDP (formerly CSDP_EXE) 2.11 - ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH) 2.12 - ISABELLE_OCAML (formerly EXEC_OCAML) 2.13 - ISABELLE_SWIPL (formerly EXEC_SWIPL) 2.14 - ISABELLE_YAP (formerly EXEC_YAP) 2.15 - 2.16 -Note that automated detection from the file-system or search path has 2.17 -been discontinued. INCOMPATIBILITY. 2.18 - 2.19 * Name space: former unsynchronized references are now proper 2.20 configuration options, with more conventional names: 2.21 2.22 @@ -162,7 +150,8 @@ 2.23 - Theory Library/Code_Char_ord provides native ordering of 2.24 characters in the target language. 2.25 2.26 - - Commands code_module and code_library are legacy, use export_code instead. 2.27 + - Commands code_module and code_library are legacy, use export_code 2.28 + instead. 2.29 2.30 - Method "evaluation" is legacy, use method "eval" instead. 2.31 2.32 @@ -173,8 +162,8 @@ 2.33 2.34 * Declare ext [intro] by default. Rare INCOMPATIBILITY. 2.35 2.36 -* The misleading name fastsimp has been renamed to fastforce, 2.37 - but fastsimp is still available as a legacy feature. 2.38 +* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is 2.39 +still available as a legacy feature for some time. 2.40 2.41 * Nitpick: 2.42 - Added "need" and "total_consts" options. 2.43 @@ -184,20 +173,21 @@ 2.44 2.45 * Sledgehammer: 2.46 - Use quasi-sound (and efficient) translations by default. 2.47 - - Added support for the following provers: E-ToFoF, LEO-II, Satallax, SNARK, 2.48 - Waldmeister, and Z3 with TPTP syntax. 2.49 - - Automatically preplay and minimize proofs before showing them if this can be 2.50 - done within reasonable time. 2.51 + - Added support for the following provers: E-ToFoF, LEO-II, 2.52 + Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax. 2.53 + - Automatically preplay and minimize proofs before showing them if 2.54 + this can be done within reasonable time. 2.55 - sledgehammer available_provers ~> sledgehammer supported_provers. 2.56 INCOMPATIBILITY. 2.57 - - Added "preplay_timeout", "slicing", "type_enc", "sound", "max_mono_iters", 2.58 - and "max_new_mono_instances" options. 2.59 - - Removed "explicit_apply" and "full_types" options as well as "Full Types" 2.60 - Proof General menu item. INCOMPATIBILITY. 2.61 + - Added "preplay_timeout", "slicing", "type_enc", "sound", 2.62 + "max_mono_iters", and "max_new_mono_instances" options. 2.63 + - Removed "explicit_apply" and "full_types" options as well as "Full 2.64 + Types" Proof General menu item. INCOMPATIBILITY. 2.65 2.66 * Metis: 2.67 - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. 2.68 - - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY. 2.69 + - Obsoleted "metisFT" -- use "metis (full_types)" instead. 2.70 + INCOMPATIBILITY. 2.71 2.72 * Command 'try': 2.73 - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and 2.74 @@ -206,23 +196,19 @@ 2.75 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. 2.76 2.77 * Quickcheck: 2.78 - 2.79 - Added "eval" option to evaluate terms for the found counterexample 2.80 (currently only supported by the default (exhaustive) tester). 2.81 - 2.82 - Added post-processing of terms to obtain readable counterexamples 2.83 (currently only supported by the default (exhaustive) tester). 2.84 - 2.85 - New counterexample generator quickcheck[narrowing] enables 2.86 narrowing-based testing. Requires the Glasgow Haskell compiler 2.87 with its installation location defined in the Isabelle settings 2.88 environment as ISABELLE_GHC. 2.89 - 2.90 - Removed quickcheck tester "SML" based on the SML code generator 2.91 (formly in HOL/Library). 2.92 2.93 -* Function package: discontinued option "tailrec". 2.94 -INCOMPATIBILITY. Use 'partial_function' instead. 2.95 +* Function package: discontinued option "tailrec". INCOMPATIBILITY, 2.96 +use 'partial_function' instead. 2.97 2.98 * Session HOL-Probability: 2.99 - Caratheodory's extension lemma is now proved for ring_of_sets. 2.100 @@ -231,9 +217,9 @@ 2.101 - Use extended reals instead of positive extended 2.102 reals. INCOMPATIBILITY. 2.103 2.104 -* Theory Library/Extended_Reals replaces now the positive extended reals 2.105 - found in probability theory. This file is extended by 2.106 - Multivariate_Analysis/Extended_Real_Limits. 2.107 +* Theory Library/Extended_Reals replaces now the positive extended 2.108 +reals found in probability theory. This file is extended by 2.109 +Multivariate_Analysis/Extended_Real_Limits. 2.110 2.111 * Old 'recdef' package has been moved to theory Library/Old_Recdef, 2.112 from where it must be imported explicitly. INCOMPATIBILITY. 2.113 @@ -241,12 +227,12 @@ 2.114 * Well-founded recursion combinator "wfrec" has been moved to theory 2.115 Library/Wfrec. INCOMPATIBILITY. 2.116 2.117 -* Theory HOL/Library/Cset_Monad allows do notation for computable 2.118 - sets (cset) via the generic monad ad-hoc overloading facility. 2.119 +* Theory HOL/Library/Cset_Monad allows do notation for computable sets 2.120 +(cset) via the generic monad ad-hoc overloading facility. 2.121 2.122 * Theories of common data structures are split into theories for 2.123 - implementation, an invariant-ensuring type, and connection to 2.124 - an abstract type. INCOMPATIBILITY. 2.125 +implementation, an invariant-ensuring type, and connection to an 2.126 +abstract type. INCOMPATIBILITY. 2.127 2.128 - RBT is split into RBT and RBT_Mapping. 2.129 - AssocList is split and renamed into AList and AList_Mapping. 2.130 @@ -423,9 +409,9 @@ 2.131 bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero 2.132 LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at] 2.133 2.134 -* Theory Complex_Main: The definition of infinite series was generalized. 2.135 - Now it is defined on the type class {topological_space, comm_monoid_add}. 2.136 - Hence it is useable also for extended real numbers. 2.137 +* Theory Complex_Main: The definition of infinite series was 2.138 +generalized. Now it is defined on the type class {topological_space, 2.139 +comm_monoid_add}. Hence it is useable also for extended real numbers. 2.140 2.141 * Theory Complex_Main: The complex exponential function "expi" is now 2.142 a type-constrained abbreviation for "exp :: complex => complex"; thus 2.143 @@ -434,12 +420,6 @@ 2.144 2.145 *** Document preparation *** 2.146 2.147 -* Localized \isabellestyle switch can be used within blocks or groups 2.148 -like this: 2.149 - 2.150 - \isabellestyle{it} %preferred default 2.151 - {\isabellestylett @{text "typewriter stuff"}} 2.152 - 2.153 * Antiquotation @{rail} layouts railroad syntax diagrams, see also 2.154 isar-ref manual, both for description and actual application of the 2.155 same. 2.156 @@ -454,9 +434,15 @@ 2.157 * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then> 2.158 (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). 2.159 2.160 -* Discontinued special treatment of hard tabulators, which are better 2.161 -avoided in the first place (no universally agreed standard expansion). 2.162 -Implicit tab-width is now 1. 2.163 +* Localized \isabellestyle switch can be used within blocks or groups 2.164 +like this: 2.165 + 2.166 + \isabellestyle{it} %preferred default 2.167 + {\isabellestylett @{text "typewriter stuff"}} 2.168 + 2.169 +* Discontinued special treatment of hard tabulators. Implicit 2.170 +tab-width is now defined as 1. Potential INCOMPATIBILITY for visual 2.171 +layouts. 2.172 2.173 2.174 *** ML *** 2.175 @@ -519,14 +505,26 @@ 2.176 2.177 *** System *** 2.178 2.179 +* Various optional external tools are referenced more robustly and 2.180 +uniformly by explicit Isabelle settings as follows: 2.181 + 2.182 + ISABELLE_CSDP (formerly CSDP_EXE) 2.183 + ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH) 2.184 + ISABELLE_OCAML (formerly EXEC_OCAML) 2.185 + ISABELLE_SWIPL (formerly EXEC_SWIPL) 2.186 + ISABELLE_YAP (formerly EXEC_YAP) 2.187 + 2.188 +Note that automated detection from the file-system or search path has 2.189 +been discontinued. INCOMPATIBILITY. 2.190 + 2.191 * Scala layer provides JVM method invocation service for static 2.192 methods of type (String)String, see Invoke_Scala.method in ML. For 2.193 example: 2.194 2.195 Invoke_Scala.method "java.lang.System.getProperty" "java.home" 2.196 2.197 -Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this 2.198 -allows to pass structured values between ML and Scala. 2.199 +Together with YXML.string_of_body/parse_body and XML.Encode/Decode 2.200 +this allows to pass structured values between ML and Scala. 2.201 2.202 * The IsabelleText fonts includes some further glyphs to support the 2.203 Prover IDE. Potential INCOMPATIBILITY: users who happen to have