author | wenzelm |

Sun Nov 22 14:13:18 2009 +0100 (2009-11-22 ago) | |

changeset 33842 | efa1b89c79e0 |

parent 33841 | 6508d0e8bb19 |

child 33843 | 23d09560d56d |

misc tuning and updates for official release;

ANNOUNCE | file | annotate | diff | revisions | |

CONTRIBUTORS | file | annotate | diff | revisions | |

NEWS | file | annotate | diff | revisions | |

README | file | annotate | diff | revisions |

1.1 --- a/ANNOUNCE Sat Nov 21 20:44:16 2009 +0100 1.2 +++ b/ANNOUNCE Sun Nov 22 14:13:18 2009 +0100 1.3 @@ -1,40 +1,16 @@ 1.4 -Subject: Announcing Isabelle2009 1.5 +Subject: Announcing Isabelle2009-1 1.6 To: isabelle-users@cl.cam.ac.uk 1.7 1.8 -Isabelle2009 is now available. 1.9 +Isabelle2009-1 is now available. 1.10 1.11 -This release significantly improves upon Isabelle2008, see the NEWS 1.12 +This release improves upon Isabelle2009 in many ways, see the NEWS 1.13 file in the distribution for more details. Some important changes 1.14 are: 1.15 1.16 -* Complete re-implementation of locales, with proper support for local 1.17 -syntax, and more general locale expressions. 1.18 - 1.19 -* New 'find_consts' and 'find_theorems' facilities, together with 1.20 -"auto solve" feature of toplevel goal statements. 1.21 - 1.22 -* HOL: reorganization of main logic images. 1.23 - 1.24 -* HOL: improved implementation of Sledgehammer, based on generic ATP 1.25 -manager; support for remote ATPs. 1.26 - 1.27 -* HOL: numerous library improvements. 1.28 - 1.29 -* Updated and extended versions of main reference manuals. 1.30 - 1.31 -* Simplified arrangement of Isabelle startup scripts and settings 1.32 -directory. 1.33 - 1.34 -* Simplified programming interfaces for all Isar language elements. 1.35 - 1.36 -* General high-level support for concurrent ML programming. 1.37 - 1.38 -* Parallel proof checking within Isar theories. 1.39 - 1.40 -* Haskabelle importer from Haskell source files to Isar theories. 1.41 +* FIXME 1.42 1.43 1.44 -You may get Isabelle2009 from the following mirror sites: 1.45 +You may get Isabelle2009-1 from the following mirror sites: 1.46 1.47 Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ 1.48 Munich (Germany) http://isabelle.in.tum.de/

2.1 --- a/CONTRIBUTORS Sat Nov 21 20:44:16 2009 +0100 2.2 +++ b/CONTRIBUTORS Sun Nov 22 14:13:18 2009 +0100 2.3 @@ -4,23 +4,24 @@ 2.4 distribution. 2.5 2.6 2.7 -Contributions to this Isabelle version 2.8 --------------------------------------- 2.9 +Contributions to Isabelle2009-1 2.10 +------------------------------- 2.11 2.12 * November 2009: Robert Himmelmann, TUM 2.13 Derivation and Brouwer's fixpoint theorem in Multivariate Analysis 2.14 2.15 -* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM 2.16 - A tabled implementation of the reflexive transitive closure 2.17 +* November 2009: Stefan Berghofer and Lukas Bulwahn, TUM 2.18 + A tabled implementation of the reflexive transitive closure. 2.19 2.20 * November 2009: Lukas Bulwahn, TUM 2.21 - Predicate Compiler: a compiler for inductive predicates to equational specfications 2.22 + Predicate Compiler: a compiler for inductive predicates to 2.23 + equational specfications. 2.24 2.25 * November 2009: Sascha Boehme, TUM 2.26 - HOL-Boogie: an interactive prover back-end for Boogie and VCC 2.27 + HOL-Boogie: an interactive prover back-end for Boogie and VCC. 2.28 2.29 * October 2009: Jasmin Blanchette, TUM 2.30 - Nitpick: yet another counterexample generator for Isabelle/HOL 2.31 + Nitpick: yet another counterexample generator for Isabelle/HOL. 2.32 2.33 * October 2009: Sascha Boehme, TUM 2.34 Extension of SMT method: proof-reconstruction for the SMT solver Z3.

3.1 --- a/NEWS Sat Nov 21 20:44:16 2009 +0100 3.2 +++ b/NEWS Sun Nov 22 14:13:18 2009 +0100 3.3 @@ -1,8 +1,8 @@ 3.4 Isabelle NEWS -- history user-relevant changes 3.5 ============================================== 3.6 3.7 -New in this Isabelle version 3.8 ----------------------------- 3.9 +New in Isabelle2009-1 (December 2009) 3.10 +------------------------------------- 3.11 3.12 *** General *** 3.13 3.14 @@ -19,74 +19,77 @@ 3.15 The currently only available mixins are the equations used to map 3.16 local definitions to terms of the target domain of an interpretation. 3.17 3.18 -* Reactivated diagnositc command 'print_interps'. Use 'print_interps l' 3.19 -to print all interpretations of locale l in the theory. Interpretations 3.20 -in proofs are not shown. 3.21 +* Reactivated diagnostic command 'print_interps'. Use "print_interps 3.22 +loc" to print all interpretations of locale "loc" in the theory. 3.23 +Interpretations in proofs are not shown. 3.24 3.25 * Thoroughly revised locales tutorial. New section on conditional 3.26 interpretation. 3.27 3.28 3.29 -*** document preparation *** 3.30 - 3.31 -* New generalized style concept for printing terms: 3.32 -write @{foo (style) ...} instead of @{foo_style style ...} 3.33 -(old form is still retained for backward compatibility). 3.34 -Styles can be also applied for antiquotations prop, term_type and typeof. 3.35 +*** Document preparation *** 3.36 + 3.37 +* New generalized style concept for printing terms: @{foo (style) ...} 3.38 +instead of @{foo_style style ...} (old form is still retained for 3.39 +backward compatibility). Styles can be also applied for 3.40 +antiquotations prop, term_type and typeof. 3.41 3.42 3.43 *** HOL *** 3.44 3.45 -* A tabled implementation of the reflexive transitive closure 3.46 - 3.47 -* New commands "code_pred" and "values" to invoke the predicate compiler 3.48 -and to enumerate values of inductive predicates. 3.49 - 3.50 -* Combined former theories Divides and IntDiv to one theory Divides 3.51 -in the spirit of other number theory theories in HOL; some constants 3.52 -(and to a lesser extent also facts) have been suffixed with _nat und _int 3.53 +* A tabled implementation of the reflexive transitive closure. 3.54 + 3.55 +* New commands 'code_pred' and 'values' to invoke the predicate 3.56 +compiler and to enumerate values of inductive predicates. 3.57 + 3.58 +* Combined former theories Divides and IntDiv to one theory Divides in 3.59 +the spirit of other number theory theories in HOL; some constants (and 3.60 +to a lesser extent also facts) have been suffixed with _nat and _int 3.61 respectively. INCOMPATIBILITY. 3.62 3.63 -* Most rules produced by inductive and datatype package 3.64 -have mandatory prefixes. 3.65 -INCOMPATIBILITY. 3.66 - 3.67 -* New proof method "smt" for a combination of first-order logic 3.68 -with equality, linear and nonlinear (natural/integer/real) 3.69 -arithmetic, and fixed-size bitvectors; there is also basic 3.70 -support for higher-order features (esp. lambda abstractions). 3.71 -It is an incomplete decision procedure based on external SMT 3.72 -solvers using the oracle mechanism; for the SMT solver Z3, 3.73 -this method is proof-producing. Certificates are provided to 3.74 -avoid calling the external solvers solely for re-checking proofs. 3.75 -Due to a remote SMT service there is no need for installing SMT 3.76 -solvers locally. 3.77 - 3.78 -* New commands to load and prove verification conditions 3.79 -generated by the Boogie program verifier or derived systems 3.80 -(e.g. the Verifying C Compiler (VCC) or Spec#). 3.81 - 3.82 -* New counterexample generator tool "nitpick" based on the Kodkod 3.83 -relational model finder. 3.84 - 3.85 -* Reorganization of number theory: 3.86 - * former session NumberTheory now named Old_Number_Theory 3.87 - * new session Number_Theory by Jeremy Avigad; if possible, prefer this. 3.88 - * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/; 3.89 - * moved theory Pocklington from Library/ to Old_Number_Theory/; 3.90 - * removed various references to Old_Number_Theory from HOL distribution. 3.91 -INCOMPATIBILITY. 3.92 +* Most rules produced by inductive and datatype package have mandatory 3.93 +prefixes. INCOMPATIBILITY. 3.94 + 3.95 +* New proof method "smt" for a combination of first-order logic with 3.96 +equality, linear and nonlinear (natural/integer/real) arithmetic, and 3.97 +fixed-size bitvectors; there is also basic support for higher-order 3.98 +features (esp. lambda abstractions). It is an incomplete decision 3.99 +procedure based on external SMT solvers using the oracle mechanism; 3.100 +for the SMT solver Z3, this method is proof-producing. Certificates 3.101 +are provided to avoid calling the external solvers solely for 3.102 +re-checking proofs. Due to a remote SMT service there is no need for 3.103 +installing SMT solvers locally. See src/HOL/SMT. 3.104 + 3.105 +* New commands to load and prove verification conditions generated by 3.106 +the Boogie program verifier or derived systems (e.g. the Verifying C 3.107 +Compiler (VCC) or Spec#). See src/HOL/Boogie. 3.108 + 3.109 +* New counterexample generator tool 'nitpick' based on the Kodkod 3.110 +relational model finder. See src/HOL/Tools/Nitpick and 3.111 +src/HOL/Nitpick_Examples. 3.112 + 3.113 +* Reorganization of number theory, INCOMPATIBILITY: 3.114 + - former session NumberTheory now named Old_Number_Theory 3.115 + - new session Number_Theory; prefer this, if possible 3.116 + - moved legacy theories Legacy_GCD and Primes from src/HOL/Library 3.117 + to src/HOL/Old_Number_Theory 3.118 + - moved theory Pocklington from src/HOL/Library to 3.119 + src/HOL/Old_Number_Theory 3.120 + - removed various references to Old_Number_Theory from HOL 3.121 + distribution 3.122 3.123 * Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm 3.124 of finite and infinite sets. It is shown that they form a complete 3.125 lattice. 3.126 3.127 -* New theory SupInf of the supremum and infimum operators for sets of reals. 3.128 - 3.129 -* New theory Probability, which contains a development of measure theory, eventually leading to Lebesgue integration and probability. 3.130 - 3.131 -* Split off prime number ingredients from theory GCD 3.132 -to theory Number_Theory/Primes; 3.133 +* Split off prime number ingredients from theory GCD to theory 3.134 +Number_Theory/Primes. 3.135 + 3.136 +* New theory SupInf of the supremum and infimum operators for sets of 3.137 +reals. 3.138 + 3.139 +* New theory Probability, which contains a development of measure 3.140 +theory, eventually leading to Lebesgue integration and probability. 3.141 3.142 * Class semiring_div requires superclass no_zero_divisors and proof of 3.143 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, 3.144 @@ -96,32 +99,33 @@ 3.145 zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. 3.146 INCOMPATIBILITY. 3.147 3.148 -* Extended Multivariate Analysis to include derivation and Brouwer's fixpoint 3.149 -theorem. 3.150 - 3.151 -* Removed predicate "M hassize n" (<--> card M = n & finite M). Was only used 3.152 -in Multivariate Analysis. Renamed vector_less_eq_def to vector_le_def, the 3.153 -more usual name. 3.154 +* Extended Multivariate Analysis to include derivation and Brouwer's 3.155 +fixpoint theorem. 3.156 + 3.157 +* Removed predicate "M hassize n" (<--> card M = n & finite M). 3.158 +INCOMPATIBILITY. 3.159 + 3.160 +* Renamed vector_less_eq_def to vector_le_def, the more usual name. 3.161 INCOMPATIBILITY. 3.162 3.163 -* Added theorem List.map_map as [simp]. Removed List.map_compose. 3.164 +* Added theorem List.map_map as [simp]. Removed List.map_compose. 3.165 INCOMPATIBILITY. 3.166 3.167 -* New testing tool "Mirabelle" for automated (proof) tools. Applies 3.168 +* New testing tool "Mirabelle" for automated proof tools. Applies 3.169 several tools and tactics like sledgehammer, metis, or quickcheck, to 3.170 -every proof step in a theory. To be used in batch mode via the 3.171 +every proof step in a theory. To be used in batch mode via the 3.172 "mirabelle" utility. 3.173 3.174 * New proof method "sos" (sum of squares) for nonlinear real 3.175 -arithmetic (originally due to John Harison). It requires 3.176 +arithmetic (originally due to John Harison). It requires theory 3.177 Library/Sum_Of_Squares. It is not a complete decision procedure but 3.178 works well in practice on quantifier-free real arithmetic with +, -, 3.179 *, ^, =, <= and <, i.e. boolean combinations of equalities and 3.180 -inequalities between polynomials. It makes use of external 3.181 -semidefinite programming solvers. Method "sos" generates a certificate 3.182 -that can be pasted into the proof thus avoiding the need to call an external 3.183 -tool every time the proof is checked. 3.184 -For more information and examples see src/HOL/Library/Sum_Of_Squares. 3.185 +inequalities between polynomials. It makes use of external 3.186 +semidefinite programming solvers. Method "sos" generates a 3.187 +certificate that can be pasted into the proof thus avoiding the need 3.188 +to call an external tool every time the proof is checked. See 3.189 +src/HOL/Library/Sum_Of_Squares. 3.190 3.191 * Code generator attributes follow the usual underscore convention: 3.192 code_unfold replaces code unfold 3.193 @@ -132,12 +136,15 @@ 3.194 * Refinements to lattice classes and sets: 3.195 - less default intro/elim rules in locale variant, more default 3.196 intro/elim rules in class variant: more uniformity 3.197 - - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff 3.198 - - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci) 3.199 + - lemma ge_sup_conv renamed to le_sup_iff, in accordance with 3.200 + le_inf_iff 3.201 + - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and 3.202 + sup_aci) 3.203 - renamed ACI to inf_sup_aci 3.204 - new class "boolean_algebra" 3.205 - - class "complete_lattice" moved to separate theory "complete_lattice"; 3.206 - corresponding constants (and abbreviations) renamed and with authentic syntax: 3.207 + - class "complete_lattice" moved to separate theory 3.208 + "complete_lattice"; corresponding constants (and abbreviations) 3.209 + renamed and with authentic syntax: 3.210 Set.Inf ~> Complete_Lattice.Inf 3.211 Set.Sup ~> Complete_Lattice.Sup 3.212 Set.INFI ~> Complete_Lattice.INFI 3.213 @@ -164,111 +171,101 @@ 3.214 - object-logic definitions as far as appropriate 3.215 3.216 INCOMPATIBILITY. Care is required when theorems Int_subset_iff or 3.217 -Un_subset_iff are explicitly deleted as default simp rules; then 3.218 -also their lattice counterparts le_inf_iff and le_sup_iff have to be 3.219 +Un_subset_iff are explicitly deleted as default simp rules; then also 3.220 +their lattice counterparts le_inf_iff and le_sup_iff have to be 3.221 deleted to achieve the desired effect. 3.222 3.223 -* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no 3.224 -simp rules by default any longer. The same applies to 3.225 -min_max.inf_absorb1 etc.! INCOMPATIBILITY. 3.226 - 3.227 -* sup_Int_eq and sup_Un_eq are no default pred_set_conv rules any longer. 3.228 -INCOMPATIBILITY. 3.229 - 3.230 -* Power operations on relations and functions are now one dedicate 3.231 +* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp 3.232 +rules by default any longer; the same applies to min_max.inf_absorb1 3.233 +etc. INCOMPATIBILITY. 3.234 + 3.235 +* Rules sup_Int_eq and sup_Un_eq are no longer declared as 3.236 +pred_set_conv by default. INCOMPATIBILITY. 3.237 + 3.238 +* Power operations on relations and functions are now one dedicated 3.239 constant "compow" with infix syntax "^^". Power operation on 3.240 multiplicative monoids retains syntax "^" and is now defined generic 3.241 in class power. INCOMPATIBILITY. 3.242 3.243 -* Relation composition "R O S" now has a "more standard" argument 3.244 -order, i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }". 3.245 -INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs 3.246 -may occationally break, since the O_assoc rule was not rewritten like 3.247 -this. Fix using O_assoc[symmetric]. The same applies to the curried 3.248 -version "R OO S". 3.249 +* Relation composition "R O S" now has a more standard argument order: 3.250 +"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}". INCOMPATIBILITY, 3.251 +rewrite propositions with "S O R" --> "R O S". Proofs may occasionally 3.252 +break, since the O_assoc rule was not rewritten like this. Fix using 3.253 +O_assoc[symmetric]. The same applies to the curried version "R OO S". 3.254 3.255 * Function "Inv" is renamed to "inv_into" and function "inv" is now an 3.256 -abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. 3.257 +abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. 3.258 INCOMPATIBILITY. 3.259 3.260 * ML antiquotation @{code_datatype} inserts definition of a datatype 3.261 -generated by the code generator; see Predicate.thy for an example. 3.262 +generated by the code generator; e.g. see src/HOL/Predicate.thy. 3.263 3.264 * New method "linarith" invokes existing linear arithmetic decision 3.265 procedure only. 3.266 3.267 * New implementation of quickcheck uses generic code generator; 3.268 default generators are provided for all suitable HOL types, records 3.269 -and datatypes. Old quickcheck can be re-activated importing 3.270 -theory Library/SML_Quickcheck. 3.271 +and datatypes. Old quickcheck can be re-activated importing theory 3.272 +Library/SML_Quickcheck. 3.273 3.274 * Renamed theorems: 3.275 Suc_eq_add_numeral_1 -> Suc_eq_plus1 3.276 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left 3.277 Suc_plus1 -> Suc_eq_plus1 3.278 3.279 -* Moved theorems: 3.280 -Wellfounded.in_inv_image -> Relation.in_inv_image 3.281 - 3.282 * New sledgehammer option "Full Types" in Proof General settings menu. 3.283 Causes full type information to be output to the ATPs. This slows 3.284 ATPs down considerably but eliminates a source of unsound "proofs" 3.285 that fail later. 3.286 3.287 -* New method metisFT: A version of metis that uses full type information 3.288 -in order to avoid failures of proof reconstruction. 3.289 - 3.290 -* Discontinued ancient tradition to suffix certain ML module names 3.291 -with "_package", e.g.: 3.292 - 3.293 - DatatypePackage ~> Datatype 3.294 - InductivePackage ~> Inductive 3.295 - 3.296 -INCOMPATIBILITY. 3.297 - 3.298 -* Discontinued abbreviation "arbitrary" of constant 3.299 -"undefined". INCOMPATIBILITY, use "undefined" directly. 3.300 +* New method "metisFT": A version of metis that uses full type 3.301 +information in order to avoid failures of proof reconstruction. 3.302 + 3.303 +* Discontinued abbreviation "arbitrary" of constant "undefined". 3.304 +INCOMPATIBILITY, use "undefined" directly. 3.305 3.306 * New evaluator "approximate" approximates an real valued term using 3.307 the same method as the approximation method. 3.308 3.309 -* Method "approximate" supports now arithmetic expressions as 3.310 +* Method "approximate" now supports arithmetic expressions as 3.311 boundaries of intervals and implements interval splitting and Taylor 3.312 series expansion. 3.313 3.314 -* Changed DERIV_intros to a dynamic fact (via Named_Thms). Each of 3.315 -the theorems in DERIV_intros assumes composition with an additional 3.316 -function and matches a variable to the derivative, which has to be 3.317 -solved by the simplifier. Hence (auto intro!: DERIV_intros) computes 3.318 -the derivative of most elementary terms. 3.319 - 3.320 -* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are 3.321 -replaced by: (auto intro!: DERIV_intros). INCOMPATIBILITY. 3.322 +* Changed "DERIV_intros" to a dynamic fact, which can be augmented by 3.323 +the attribute of the same name. Each of the theorems in the list 3.324 +DERIV_intros assumes composition with an additional function and 3.325 +matches a variable to the derivative, which has to be solved by the 3.326 +Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative 3.327 +of most elementary terms. 3.328 + 3.329 +* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded 3.330 +are replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY. 3.331 3.332 * Renamed methods: 3.333 sizechange -> size_change 3.334 induct_scheme -> induction_schema 3.335 3.336 * Lemma name change: replaced "anti_sym" by "antisym" everywhere. 3.337 +INCOMPATIBILITY. 3.338 3.339 3.340 *** HOLCF *** 3.341 3.342 -* Theory 'Representable.thy' defines a class 'rep' of domains that are 3.343 -representable (via an ep-pair) in the universal domain type 'udom'. 3.344 +* Theory Representable defines a class "rep" of domains that are 3.345 +representable (via an ep-pair) in the universal domain type "udom". 3.346 Instances are provided for all type constructors defined in HOLCF. 3.347 3.348 * The 'new_domain' command is a purely definitional version of the 3.349 domain package, for representable domains. Syntax is identical to the 3.350 old domain package. The 'new_domain' package also supports indirect 3.351 recursion using previously-defined type constructors. See 3.352 -HOLCF/ex/New_Domain.thy for examples. 3.353 - 3.354 -* Method 'fixrec_simp' unfolds one step of a fixrec-defined constant 3.355 +src/HOLCF/ex/New_Domain.thy for examples. 3.356 + 3.357 +* Method "fixrec_simp" unfolds one step of a fixrec-defined constant 3.358 on the left-hand side of an equation, and then performs 3.359 simplification. Rewriting is done using rules declared with the 3.360 -'fixrec_simp' attribute. The 'fixrec_simp' method is intended as a 3.361 -replacement for 'fixpat'; see HOLCF/ex/Fixrec_ex.thy for examples. 3.362 +"fixrec_simp" attribute. The "fixrec_simp" method is intended as a 3.363 +replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples. 3.364 3.365 * The pattern-match compiler in 'fixrec' can now handle constructors 3.366 with HOL function types. Pattern-match combinators for the Pair 3.367 @@ -280,13 +277,13 @@ 3.368 3.369 * The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has 3.370 been renamed to "below". The name "below" now replaces "less" in many 3.371 -theorem names. (Legacy theorem names using "less" are still 3.372 -supported as well.) 3.373 +theorem names. (Legacy theorem names using "less" are still supported 3.374 +as well.) 3.375 3.376 * The 'fixrec' package now supports "bottom patterns". Bottom 3.377 patterns can be used to generate strictness rules, or to make 3.378 functions more strict (much like the bang-patterns supported by the 3.379 -Glasgow Haskell Compiler). See HOLCF/ex/Fixrec_ex.thy for examples. 3.380 +Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for examples. 3.381 3.382 3.383 *** ML *** 3.384 @@ -296,9 +293,6 @@ 3.385 to be pure, but the old TheoryDataFun for mutable data (with explicit 3.386 copy operation) is still available for some time. 3.387 3.388 -* Removed some old-style infix operations using polymorphic equality. 3.389 -INCOMPATIBILITY. 3.390 - 3.391 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML) 3.392 provides a high-level programming interface to synchronized state 3.393 variables with atomic update. This works via pure function 3.394 @@ -330,8 +324,11 @@ 3.395 3.396 * Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY. 3.397 3.398 +* Renamed several structures FooBar to Foo_Bar. Occasional, 3.399 +INCOMPATIBILITY. 3.400 + 3.401 * Eliminated old Attrib.add_attributes, Method.add_methods and related 3.402 -cominators for "args". INCOMPATIBILITY, need to use simplified 3.403 +combinators for "args". INCOMPATIBILITY, need to use simplified 3.404 Attrib/Method.setup introduced in Isabelle2009. 3.405 3.406 * Proper context for simpset_of, claset_of, clasimpset_of. May fall 3.407 @@ -347,29 +344,30 @@ 3.408 Syntax.pretty_typ/term directly, preferably with proper context 3.409 instead of global theory. 3.410 3.411 -* Operations of structure Skip_Proof (formerly SkipProof) no longer 3.412 -require quick_and_dirty mode, which avoids critical setmp. 3.413 +* Operations of structure Skip_Proof no longer require quick_and_dirty 3.414 +mode, which avoids critical setmp. 3.415 3.416 3.417 *** System *** 3.418 3.419 +* Further fine tuning of parallel proof checking, scales up to 8 cores 3.420 +(max. speedup factor 5.0). See also Goal.parallel_proofs in ML and 3.421 +usedir option -q. 3.422 + 3.423 * Support for additional "Isabelle components" via etc/components, see 3.424 also the system manual. 3.425 3.426 * The isabelle makeall tool now operates on all components with 3.427 IsaMakefile, not just hardwired "logics". 3.428 3.429 -* New component "isabelle wwwfind [start|stop|status] [HEAP]" 3.430 -Provides web interface for find_theorems on HEAP. Depends on lighttpd 3.431 -webserver being installed. Currently supported on Linux only. 3.432 +* Removed "compress" option from isabelle-process and isabelle usedir; 3.433 +this is always enabled. 3.434 3.435 * Discontinued support for Poly/ML 4.x versions. 3.436 3.437 -* Removed "compress" option from isabelle-process and isabelle usedir; 3.438 -this is always enabled. 3.439 - 3.440 -* More fine-grained control of proof parallelism, cf. 3.441 -Goal.parallel_proofs in ML and usedir option -q LEVEL. 3.442 +* Isabelle tool "wwwfind" provides web interface for 'find_theorems' 3.443 +on a given logic image. This requires the lighttpd webserver and is 3.444 +currently supported on Linux only. 3.445 3.446 3.447

4.1 --- a/README Sat Nov 21 20:44:16 2009 +0100 4.2 +++ b/README Sun Nov 22 14:13:18 2009 +0100 4.3 @@ -11,11 +11,11 @@ 4.4 4.5 Isabelle requires a regular Unix platform (e.g. GNU Linux) with the 4.6 following additional software: 4.7 - * A full Standard ML Compiler (works best with Poly/ML 5.2.1). 4.8 + 4.9 + * A full Standard ML Compiler (works best with Poly/ML 5.3.0). 4.10 * The GNU bash shell (version 3.x or 2.x). 4.11 * Perl (version 5.x). 4.12 - * GNU Emacs (version 21, 22, 23) or XEmacs (version 21.4.x) 4.13 - -- for the Proof General interface. 4.14 + * GNU Emacs (version 22 or 23) -- for the Proof General interface. 4.15 * A complete LaTeX installation -- for document preparation. 4.16 4.17 Installation