misc tuning and updates for official release;
authorwenzelm
Sun Nov 22 14:13:18 2009 +0100 (2009-11-22)
changeset 33842efa1b89c79e0
parent 33841 6508d0e8bb19
child 33843 23d09560d56d
misc tuning and updates for official release;
ANNOUNCE
CONTRIBUTORS
NEWS
README
     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