NEWS

 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
-New in this Isabelle version
-----------------------------
+New in Isabelle2009-1 (December 2009)
+-------------------------------------
 
 *** General ***
 
 * Discontinued old form of "escaped symbols" such as \\<forall>.  Only
 one backslash should be used, even in ML sources.

 
 * Locale interpretation propagates mixins along the locale hierarchy.
 The currently only available mixins are the equations used to map
 local definitions to terms of the target domain of an interpretation.
 
-* Reactivated diagnositc command 'print_interps'.  Use 'print_interps l'
-to print all interpretations of locale l in the theory.  Interpretations
-in proofs are not shown.
+* Reactivated diagnostic command 'print_interps'.  Use "print_interps
+loc" to print all interpretations of locale "loc" in the theory.
+Interpretations in proofs are not shown.
 
 * Thoroughly revised locales tutorial.  New section on conditional
 interpretation.
 
 
-*** document preparation ***
-
-* New generalized style concept for printing terms:
-write @{foo (style) ...} instead of @{foo_style style ...}
-(old form is still retained for backward compatibility).
-Styles can be also applied for antiquotations prop, term_type and typeof.
+*** Document preparation ***
+
+* New generalized style concept for printing terms: @{foo (style) ...}
+instead of @{foo_style style ...}  (old form is still retained for
+backward compatibility).  Styles can be also applied for
+antiquotations prop, term_type and typeof.
 
 
 *** HOL ***
 
-* A tabled implementation of the reflexive transitive closure
-
-* New commands "code_pred" and "values" to invoke the predicate compiler
-and to enumerate values of inductive predicates.
-
-* Combined former theories Divides and IntDiv to one theory Divides
-in the spirit of other number theory theories in HOL;  some constants
-(and to a lesser extent also facts) have been suffixed with _nat und _int
+* A tabled implementation of the reflexive transitive closure.
+
+* New commands 'code_pred' and 'values' to invoke the predicate
+compiler and to enumerate values of inductive predicates.
+
+* Combined former theories Divides and IntDiv to one theory Divides in
+the spirit of other number theory theories in HOL; some constants (and
+to a lesser extent also facts) have been suffixed with _nat and _int
 respectively.  INCOMPATIBILITY.
 
-* Most rules produced by inductive and datatype package
-have mandatory prefixes.
-INCOMPATIBILITY.
-
-* New proof method "smt" for a combination of first-order logic
-with equality, linear and nonlinear (natural/integer/real)
-arithmetic, and fixed-size bitvectors; there is also basic
-support for higher-order features (esp. lambda abstractions).
-It is an incomplete decision procedure based on external SMT
-solvers using the oracle mechanism; for the SMT solver Z3,
-this method is proof-producing. Certificates are provided to
-avoid calling the external solvers solely for re-checking proofs.
-Due to a remote SMT service there is no need for installing SMT
-solvers locally.
-
-* New commands to load and prove verification conditions
-generated by the Boogie program verifier or derived systems
-(e.g. the Verifying C Compiler (VCC) or Spec#).
-
-* New counterexample generator tool "nitpick" based on the Kodkod
-relational model finder.
-
-* Reorganization of number theory:
-  * former session NumberTheory now named Old_Number_Theory
-  * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
-  * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
-  * moved theory Pocklington from Library/ to Old_Number_Theory/;
-  * removed various references to Old_Number_Theory from HOL distribution.
-INCOMPATIBILITY.
+* Most rules produced by inductive and datatype package have mandatory
+prefixes.  INCOMPATIBILITY.
+
+* New proof method "smt" for a combination of first-order logic with
+equality, linear and nonlinear (natural/integer/real) arithmetic, and
+fixed-size bitvectors; there is also basic support for higher-order
+features (esp. lambda abstractions).  It is an incomplete decision
+procedure based on external SMT solvers using the oracle mechanism;
+for the SMT solver Z3, this method is proof-producing.  Certificates
+are provided to avoid calling the external solvers solely for
+re-checking proofs.  Due to a remote SMT service there is no need for
+installing SMT solvers locally.  See src/HOL/SMT.
+
+* New commands to load and prove verification conditions generated by
+the Boogie program verifier or derived systems (e.g. the Verifying C
+Compiler (VCC) or Spec#).  See src/HOL/Boogie.
+
+* New counterexample generator tool 'nitpick' based on the Kodkod
+relational model finder.  See src/HOL/Tools/Nitpick and
+src/HOL/Nitpick_Examples.
+
+* Reorganization of number theory, INCOMPATIBILITY:
+  - former session NumberTheory now named Old_Number_Theory
+  - new session Number_Theory; prefer this, if possible
+  - moved legacy theories Legacy_GCD and Primes from src/HOL/Library
+    to src/HOL/Old_Number_Theory
+  - moved theory Pocklington from src/HOL/Library to
+    src/HOL/Old_Number_Theory
+  - removed various references to Old_Number_Theory from HOL
+    distribution
 
 * Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
 of finite and infinite sets. It is shown that they form a complete
 lattice.
 
-* New theory SupInf of the supremum and infimum operators for sets of reals.
-
-* New theory Probability, which contains a development of measure theory, eventually leading to Lebesgue integration and probability.
-
-* Split off prime number ingredients from theory GCD
-to theory Number_Theory/Primes;
+* Split off prime number ingredients from theory GCD to theory
+Number_Theory/Primes.
+
+* New theory SupInf of the supremum and infimum operators for sets of
+reals.
+
+* New theory Probability, which contains a development of measure
+theory, eventually leading to Lebesgue integration and probability.
 
 * Class semiring_div requires superclass no_zero_divisors and proof of
 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
 generalized to class semiring_div, subsuming former theorems
 zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
 zdiv_zmult_zmult2.  div_mult_mult1 is now [simp] by default.
 INCOMPATIBILITY.
 
-* Extended Multivariate Analysis to include derivation and Brouwer's fixpoint
-theorem.
-
-* Removed predicate "M hassize n" (<--> card M = n & finite M). Was only used
-in Multivariate Analysis. Renamed vector_less_eq_def to vector_le_def, the
-more usual name.
+* Extended Multivariate Analysis to include derivation and Brouwer's
+fixpoint theorem.
+
+* Removed predicate "M hassize n" (<--> card M = n & finite M).
 INCOMPATIBILITY.
 
-* Added theorem List.map_map as [simp]. Removed List.map_compose.
+* Renamed vector_less_eq_def to vector_le_def, the more usual name.
 INCOMPATIBILITY.
 
-* New testing tool "Mirabelle" for automated (proof) tools. Applies
+* Added theorem List.map_map as [simp].  Removed List.map_compose.
+INCOMPATIBILITY.
+
+* New testing tool "Mirabelle" for automated proof tools.  Applies
 several tools and tactics like sledgehammer, metis, or quickcheck, to
-every proof step in a theory. To be used in batch mode via the
+every proof step in a theory.  To be used in batch mode via the
 "mirabelle" utility.
 
 * New proof method "sos" (sum of squares) for nonlinear real
-arithmetic (originally due to John Harison). It requires
+arithmetic (originally due to John Harison). It requires theory
 Library/Sum_Of_Squares.  It is not a complete decision procedure but
 works well in practice on quantifier-free real arithmetic with +, -,
 *, ^, =, <= and <, i.e. boolean combinations of equalities and
-inequalities between polynomials. It makes use of external
-semidefinite programming solvers. Method "sos" generates a certificate
-that can be pasted into the proof thus avoiding the need to call an external
-tool every time the proof is checked.
-For more information and examples see src/HOL/Library/Sum_Of_Squares.
+inequalities between polynomials.  It makes use of external
+semidefinite programming solvers.  Method "sos" generates a
+certificate that can be pasted into the proof thus avoiding the need
+to call an external tool every time the proof is checked.  See
+src/HOL/Library/Sum_Of_Squares.
 
 * Code generator attributes follow the usual underscore convention:
     code_unfold     replaces    code unfold
     code_post       replaces    code post
     etc.
   INCOMPATIBILITY.
 
 * Refinements to lattice classes and sets:
   - less default intro/elim rules in locale variant, more default
     intro/elim rules in class variant: more uniformity
-  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
-  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
+  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with
+    le_inf_iff
+  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and
+    sup_aci)
   - renamed ACI to inf_sup_aci
   - new class "boolean_algebra"
-  - class "complete_lattice" moved to separate theory "complete_lattice";
-    corresponding constants (and abbreviations) renamed and with authentic syntax:
+  - class "complete_lattice" moved to separate theory
+    "complete_lattice"; corresponding constants (and abbreviations)
+    renamed and with authentic syntax:
     Set.Inf ~>      Complete_Lattice.Inf
     Set.Sup ~>      Complete_Lattice.Sup
     Set.INFI ~>     Complete_Lattice.INFI
     Set.SUPR ~>     Complete_Lattice.SUPR
     Set.Inter ~>    Complete_Lattice.Inter

     Complete_Lattice.INTER  (for INFI)
     Complete_Lattice.UNION  (for SUPR)
   - object-logic definitions as far as appropriate
 
 INCOMPATIBILITY.  Care is required when theorems Int_subset_iff or
-Un_subset_iff are explicitly deleted as default simp rules;  then
-also their lattice counterparts le_inf_iff and le_sup_iff have to be
+Un_subset_iff are explicitly deleted as default simp rules; then also
+their lattice counterparts le_inf_iff and le_sup_iff have to be
 deleted to achieve the desired effect.
 
-* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no
-simp rules by default any longer.  The same applies to
-min_max.inf_absorb1 etc.!  INCOMPATIBILITY.
-
-* sup_Int_eq and sup_Un_eq are no default pred_set_conv rules any longer.
-INCOMPATIBILITY.
-
-* Power operations on relations and functions are now one dedicate
+* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp
+rules by default any longer; the same applies to min_max.inf_absorb1
+etc.  INCOMPATIBILITY.
+
+* Rules sup_Int_eq and sup_Un_eq are no longer declared as
+pred_set_conv by default.  INCOMPATIBILITY.
+
+* Power operations on relations and functions are now one dedicated
 constant "compow" with infix syntax "^^".  Power operation on
 multiplicative monoids retains syntax "^" and is now defined generic
 in class power.  INCOMPATIBILITY.
 
-* Relation composition "R O S" now has a "more standard" argument
-order, i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
-INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
-may occationally break, since the O_assoc rule was not rewritten like
-this.  Fix using O_assoc[symmetric].  The same applies to the curried
-version "R OO S".
+* Relation composition "R O S" now has a more standard argument order:
+"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}".  INCOMPATIBILITY,
+rewrite propositions with "S O R" --> "R O S". Proofs may occasionally
+break, since the O_assoc rule was not rewritten like this.  Fix using
+O_assoc[symmetric].  The same applies to the curried version "R OO S".
 
 * Function "Inv" is renamed to "inv_into" and function "inv" is now an
-abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
+abbreviation for "inv_into UNIV".  Lemmas are renamed accordingly.
 INCOMPATIBILITY.
 
 * ML antiquotation @{code_datatype} inserts definition of a datatype
-generated by the code generator; see Predicate.thy for an example.
+generated by the code generator; e.g. see src/HOL/Predicate.thy.
 
 * New method "linarith" invokes existing linear arithmetic decision
 procedure only.
 
 * New implementation of quickcheck uses generic code generator;
 default generators are provided for all suitable HOL types, records
-and datatypes.  Old quickcheck can be re-activated importing
-theory Library/SML_Quickcheck.
+and datatypes.  Old quickcheck can be re-activated importing theory
+Library/SML_Quickcheck.
 
 * Renamed theorems:
 Suc_eq_add_numeral_1 -> Suc_eq_plus1
 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
 Suc_plus1 -> Suc_eq_plus1
 
-* Moved theorems:
-Wellfounded.in_inv_image -> Relation.in_inv_image
-
 * New sledgehammer option "Full Types" in Proof General settings menu.
 Causes full type information to be output to the ATPs.  This slows
 ATPs down considerably but eliminates a source of unsound "proofs"
 that fail later.
 
-* New method metisFT: A version of metis that uses full type information
-in order to avoid failures of proof reconstruction.
-
-* Discontinued ancient tradition to suffix certain ML module names
-with "_package", e.g.:
-
-    DatatypePackage ~> Datatype
-    InductivePackage ~> Inductive
-
-INCOMPATIBILITY.
-
-* Discontinued abbreviation "arbitrary" of constant
-"undefined". INCOMPATIBILITY, use "undefined" directly.
+* New method "metisFT": A version of metis that uses full type
+information in order to avoid failures of proof reconstruction.
+
+* Discontinued abbreviation "arbitrary" of constant "undefined".
+INCOMPATIBILITY, use "undefined" directly.
 
 * New evaluator "approximate" approximates an real valued term using
 the same method as the approximation method.
 
-* Method "approximate" supports now arithmetic expressions as
+* Method "approximate" now supports arithmetic expressions as
 boundaries of intervals and implements interval splitting and Taylor
 series expansion.
 
-* Changed DERIV_intros to a dynamic fact (via Named_Thms).  Each of
-the theorems in DERIV_intros assumes composition with an additional
-function and matches a variable to the derivative, which has to be
-solved by the simplifier.  Hence (auto intro!: DERIV_intros) computes
-the derivative of most elementary terms.
-
-* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are
-replaced by: (auto intro!: DERIV_intros).  INCOMPATIBILITY.
+* Changed "DERIV_intros" to a dynamic fact, which can be augmented by
+the attribute of the same name.  Each of the theorems in the list
+DERIV_intros assumes composition with an additional function and
+matches a variable to the derivative, which has to be solved by the
+Simplifier.  Hence (auto intro!: DERIV_intros) computes the derivative
+of most elementary terms.
+
+* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded
+are replaced by (auto intro!: DERIV_intros).  INCOMPATIBILITY.
 
 * Renamed methods:
     sizechange -> size_change
     induct_scheme -> induction_schema
 
 * Lemma name change: replaced "anti_sym" by "antisym" everywhere.
+INCOMPATIBILITY.
 
 
 *** HOLCF ***
 
-* Theory 'Representable.thy' defines a class 'rep' of domains that are
-representable (via an ep-pair) in the universal domain type 'udom'.
+* Theory Representable defines a class "rep" of domains that are
+representable (via an ep-pair) in the universal domain type "udom".
 Instances are provided for all type constructors defined in HOLCF.
 
 * The 'new_domain' command is a purely definitional version of the
 domain package, for representable domains.  Syntax is identical to the
 old domain package.  The 'new_domain' package also supports indirect
 recursion using previously-defined type constructors.  See
-HOLCF/ex/New_Domain.thy for examples.
-
-* Method 'fixrec_simp' unfolds one step of a fixrec-defined constant
+src/HOLCF/ex/New_Domain.thy for examples.
+
+* Method "fixrec_simp" unfolds one step of a fixrec-defined constant
 on the left-hand side of an equation, and then performs
 simplification.  Rewriting is done using rules declared with the
-'fixrec_simp' attribute.  The 'fixrec_simp' method is intended as a
-replacement for 'fixpat'; see HOLCF/ex/Fixrec_ex.thy for examples.
+"fixrec_simp" attribute.  The "fixrec_simp" method is intended as a
+replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples.
 
 * The pattern-match compiler in 'fixrec' can now handle constructors
 with HOL function types.  Pattern-match combinators for the Pair
 constructor are pre-configured.
 

 for mutually-recursive definitions:  Induction rules have conclusions
 of the form "P foo bar" instead of "P <foo, bar>".
 
 * The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has
 been renamed to "below".  The name "below" now replaces "less" in many
-theorem names.  (Legacy theorem names using "less" are still
-supported as well.)
+theorem names.  (Legacy theorem names using "less" are still supported
+as well.)
 
 * The 'fixrec' package now supports "bottom patterns".  Bottom
 patterns can be used to generate strictness rules, or to make
 functions more strict (much like the bang-patterns supported by the
-Glasgow Haskell Compiler).  See HOLCF/ex/Fixrec_ex.thy for examples.
+Glasgow Haskell Compiler).  See src/HOLCF/ex/Fixrec_ex.thy for examples.
 
 
 *** ML ***
 
 * Theory and context data is now introduced by the simplified and
 modernized functors Theory_Data, Proof_Data, Generic_Data.  Data needs
 to be pure, but the old TheoryDataFun for mutable data (with explicit
 copy operation) is still available for some time.
-
-* Removed some old-style infix operations using polymorphic equality.
-INCOMPATIBILITY.
 
 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML)
 provides a high-level programming interface to synchronized state
 variables with atomic update.  This works via pure function
 application within a critical section -- its runtime should be as

 functors have their own ML name space there is no point to mark them
 separately.)  Minor INCOMPATIBILITY.
 
 * Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
 
+* Renamed several structures FooBar to Foo_Bar.  Occasional,
+INCOMPATIBILITY.
+
 * Eliminated old Attrib.add_attributes, Method.add_methods and related
-cominators for "args".  INCOMPATIBILITY, need to use simplified
+combinators for "args".  INCOMPATIBILITY, need to use simplified
 Attrib/Method.setup introduced in Isabelle2009.
 
 * Proper context for simpset_of, claset_of, clasimpset_of.  May fall
 back on global_simpset_of, global_claset_of, global_clasimpset_of as
 last resort.  INCOMPATIBILITY.

 
 * Discontinued Display.pretty_ctyp/cterm etc.  INCOMPATIBILITY, use
 Syntax.pretty_typ/term directly, preferably with proper context
 instead of global theory.
 
-* Operations of structure Skip_Proof (formerly SkipProof) no longer
-require quick_and_dirty mode, which avoids critical setmp.
+* Operations of structure Skip_Proof no longer require quick_and_dirty
+mode, which avoids critical setmp.
 
 
 *** System ***
+
+* Further fine tuning of parallel proof checking, scales up to 8 cores
+(max. speedup factor 5.0).  See also Goal.parallel_proofs in ML and
+usedir option -q.
 
 * Support for additional "Isabelle components" via etc/components, see
 also the system manual.
 
 * The isabelle makeall tool now operates on all components with
 IsaMakefile, not just hardwired "logics".
 
-* New component "isabelle wwwfind [start|stop|status] [HEAP]"
-Provides web interface for find_theorems on HEAP. Depends on lighttpd 
-webserver being installed. Currently supported on Linux only.
-
-* Discontinued support for Poly/ML 4.x versions.
-
 * Removed "compress" option from isabelle-process and isabelle usedir;
 this is always enabled.
 
-* More fine-grained control of proof parallelism, cf.
-Goal.parallel_proofs in ML and usedir option -q LEVEL.
+* Discontinued support for Poly/ML 4.x versions.
+
+* Isabelle tool "wwwfind" provides web interface for 'find_theorems'
+on a given logic image.  This requires the lighttpd webserver and is
+currently supported on Linux only.
 
 
 
 New in Isabelle2009 (April 2009)
 --------------------------------