# HG changeset patch # User wenzelm # Date 1335554035 -7200 # Node ID befe55c8bbdcce227e7ab1e597264502441d3176 # Parent 7e009f4e9f47b5a351d6ac0002bb195a6f4d7bb2 tuned; diff -r 7e009f4e9f47 -r befe55c8bbdc NEWS --- a/NEWS Fri Apr 27 21:02:34 2012 +0200 +++ b/NEWS Fri Apr 27 21:13:55 2012 +0200 @@ -486,10 +486,9 @@ unionwk_is_rbt -> rbt_unionwk_is_rbt unionwk_sorted -> rbt_unionwk_rbt_sorted -* Theory HOL/Library/Float: Floating point numbers are now defined as a -subset of the real numbers. All operations are defined using the -lifing-framework and proofs use the transfer method. -INCOMPATIBILITY. +* Theory HOL/Library/Float: Floating point numbers are now defined as +a subset of the real numbers. All operations are defined using the +lifing-framework and proofs use the transfer method. INCOMPATIBILITY. Changed Operations: float_abs -> abs @@ -598,13 +597,14 @@ word_of_int_0_hom ~> word_0_wi word_of_int_1_hom ~> word_1_wi -* New tactic "word_bitwise" for splitting machine word equalities and -inequalities into logical circuits. Requires theory "WordBitwise" from HOL-Word -session. Supports addition, subtraction, multiplication, shifting by -constants, bitwise operators and numeric constants. Requires fixed-length word -types, cannot operate on 'a word. Solves many standard word identies outright -and converts more into first order problems amenable to blast or similar. See -HOL/Word/WordBitwise.thy and examples in HOL/Word/Examples/WordExamples.thy. +* New proof method "word_bitwise" for splitting machine word +equalities and inequalities into logical circuits, defined in +HOL/Word/WordBitwise.thy. Supports addition, subtraction, +multiplication, shifting by constants, bitwise operators and numeric +constants. Requires fixed-length word types, not 'a word. Solves +many standard word identies outright and converts more into first +order problems amenable to blast or similar. See also examples in +HOL/Word/Examples/WordExamples.thy. * Clarified attribute "mono_set": pure declaration without modifying the result of the fact expression. @@ -658,17 +658,18 @@ * Theory Library/Multiset: Improved code generation of multisets. -* Session HOL-Probability: Introduced the type "'a measure" to represent -measures, this replaces the records 'a algebra and 'a measure_space. The -locales based on subset_class now have two locale-parameters the space -\ and the set of measurables sets M. The product of probability spaces -uses now the same constant as the finite product of sigma-finite measure -spaces "PiM :: ('i => 'a) measure". Most constants are defined now -outside of locales and gain an additional parameter, like null_sets, -almost_eventually or \'. Measure space constructions for distributions -and densities now got their own constants distr and density. Instead of -using locales to describe measure spaces with a finite space, the -measure count_space and point_measure is introduced. INCOMPATIBILITY. +* Session HOL-Probability: Introduced the type "'a measure" to +represent measures, this replaces the records 'a algebra and 'a +measure_space. The locales based on subset_class now have two +locale-parameters the space \ and the set of measurables sets +M. The product of probability spaces uses now the same constant as +the finite product of sigma-finite measure spaces "PiM :: ('i => 'a) +measure". Most constants are defined now outside of locales and gain +an additional parameter, like null_sets, almost_eventually or \'. +Measure space constructions for distributions and densities now got +their own constants distr and density. Instead of using locales to +describe measure spaces with a finite space, the measure count_space +and point_measure is introduced. INCOMPATIBILITY. Renamed constants: measure -> emeasure @@ -854,12 +855,12 @@ replaced with corresponding ones according to the transfer rules. Goals are generalized over all free variables by default; this is necessary for variables whose types changes, but can be overridden - for specific variables with e.g. 'transfer fixing: x y z'. - The variant transfer' method allows replacing a subgoal with - one that is logically stronger (rather than equivalent). + for specific variables with e.g. 'transfer fixing: x y z'. The + variant transfer' method allows replacing a subgoal with one that + is logically stronger (rather than equivalent). - relator_eq attribute: Collects identity laws for relators of - various type constructors, e.g. "list_all2 (op =) = (op =)". The + various type constructors, e.g. "list_all2 (op =) = (op =)". The transfer method uses these lemmas to infer transfer rules for non-polymorphic constants on the fly. @@ -874,8 +875,8 @@ * New Lifting package: - lift_definition command: Defines operations on an abstract type in - terms of a corresponding operation on a representation type. Example - syntax: + terms of a corresponding operation on a representation + type. Example syntax: lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" is List.insert @@ -892,11 +893,11 @@ lift_definition generates a code certificate theorem and sets up code generation for each constant. - - setup_lifting command: Sets up the Lifting package to work with - a user-defined type. The user must provide either a quotient - theorem or a type_definition theorem. The package configures - transfer rules for equality and quantifiers on the type, and sets - up the lift_definition command to work with the type. + - setup_lifting command: Sets up the Lifting package to work with a + user-defined type. The user must provide either a quotient theorem + or a type_definition theorem. The package configures transfer + rules for equality and quantifiers on the type, and sets up the + lift_definition command to work with the type. - Usage examples: See Quotient_Examples/Lift_DList.thy, Quotient_Examples/Lift_RBT.thy, Word/Word.thy and @@ -957,11 +958,11 @@ affecting 'rat' and 'real'. * Sledgehammer: - - Integrated more tightly with SPASS, as described in the ITP 2012 paper "More - SPASS with Isabelle". + - Integrated more tightly with SPASS, as described in the ITP 2012 + paper "More SPASS with Isabelle". - Made it try "smt" as a fallback if "metis" fails or times out. - - Added support for the following provers: Alt-Ergo (via Why3 and TFF1), - iProver, iProver-Eq. + - Added support for the following provers: Alt-Ergo (via Why3 and + TFF1), iProver, iProver-Eq. - Replaced remote E-SInE with remote Satallax in the default setup. - Sped up the minimizer. - Added "lam_trans", "uncurry_aliases", and "minimize" options. @@ -1058,12 +1059,12 @@ evaluated. Minor INCOMPATIBILITY: need to adapt Isabelle path where the generic user home was intended. +* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name +notation, which is useful for the jEdit file browser, for example. + * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE). -* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name -notation, which is useful for the jEdit file browser, for example. - New in Isabelle2011-1 (October 2011)