diff -r dd25b3055c4e -r 0a94e1f264ce NEWS --- a/NEWS Fri Aug 28 10:52:44 2009 +0200 +++ b/NEWS Fri Aug 28 11:31:49 2009 +0200 @@ -18,22 +18,25 @@ *** HOL *** -* 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 "isabelle mirabelle". - -* New proof method "sos" (sum of squares) for nonlinear real arithmetic -(originally due to John Harison). It requires 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. -For more information and examples see Library/Sum_Of_Squares. - -* Set.UNIV and Set.empty are mere abbreviations for top and bot. INCOMPATIBILITY. - -* More convenient names for set intersection and union. 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 +"mirabelle" utility. + +* New proof method "sos" (sum of squares) for nonlinear real +arithmetic (originally due to John Harison). It requires +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. For more information and examples +see src/HOL/Library/Sum_Of_Squares. + +* Set.UNIV and Set.empty are mere abbreviations for top and bot. +INCOMPATIBILITY. + +* More convenient names for set intersection and union. +INCOMPATIBILITY: Set.Int ~> Set.inter Set.Un ~> Set.union @@ -43,8 +46,6 @@ etc. INCOMPATIBILITY. -* New quickcheck implementation using new code generator. - * New class "boolean_algebra". * Refinements to lattices classes: @@ -81,15 +82,16 @@ 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 }". +* 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". - -* 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. +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". + +* 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. * ML antiquotation @{code_datatype} inserts definition of a datatype generated by the code generator; see Predicate.thy for an example. @@ -97,9 +99,9 @@ * New method "linarith" invokes existing linear arithmetic decision procedure only. -* Implementation of quickcheck using generic code generator; default -generators are provided for all suitable HOL types, records and -datatypes. +* New implementation of quickcheck uses generic code generator; +default generators are provided for all suitable HOL types, records +and datatypes. * Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions Set.Pow_def and Set.image_def. @@ -121,17 +123,13 @@ DatatypePackage ~> Datatype InductivePackage ~> Inductive - etc. - INCOMPATIBILITY. * NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory. If possible, use NewNumberTheory, not NumberTheory. -* Simplified interfaces of datatype module. INCOMPATIBILITY. - -* Abbreviation "arbitrary" of "undefined" has disappeared; use -"undefined" directly. INCOMPATIBILITY. +* 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. @@ -155,10 +153,14 @@ * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for parallel tactical reasoning. -* Tactical FOCUS is similar to SUBPROOF, but allows the body tactic to -introduce new subgoals and schematic variables. FOCUS_PARAMS is -similar, but focuses on the parameter prefix only, leaving subgoal -premises unchanged. +* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS +are similar to SUBPROOF, but are slightly more flexible: only the +specified parts of the subgoal are imported into the context, and the +body tactic may introduce new subgoals and schematic variables. + +* Old tactical METAHYPS, which does not observe the proof context, has +been renamed to Old_Goals.METAHYPS and awaits deletion. Use SUBPROOF +or Subgoal.FOCUS etc. * Renamed functor TableFun to Table, and GraphFun to Graph. (Since functors have their own ML name space there is no point to mark them