summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 47807 | befe55c8bbdc |

parent 47806 | 7e009f4e9f47 |

child 47809 | 4d8cbea248b0 |

1.1 --- a/NEWS Fri Apr 27 21:02:34 2012 +0200 1.2 +++ b/NEWS Fri Apr 27 21:13:55 2012 +0200 1.3 @@ -486,10 +486,9 @@ 1.4 unionwk_is_rbt -> rbt_unionwk_is_rbt 1.5 unionwk_sorted -> rbt_unionwk_rbt_sorted 1.6 1.7 -* Theory HOL/Library/Float: Floating point numbers are now defined as a 1.8 -subset of the real numbers. All operations are defined using the 1.9 -lifing-framework and proofs use the transfer method. 1.10 -INCOMPATIBILITY. 1.11 +* Theory HOL/Library/Float: Floating point numbers are now defined as 1.12 +a subset of the real numbers. All operations are defined using the 1.13 +lifing-framework and proofs use the transfer method. INCOMPATIBILITY. 1.14 1.15 Changed Operations: 1.16 float_abs -> abs 1.17 @@ -598,13 +597,14 @@ 1.18 word_of_int_0_hom ~> word_0_wi 1.19 word_of_int_1_hom ~> word_1_wi 1.20 1.21 -* New tactic "word_bitwise" for splitting machine word equalities and 1.22 -inequalities into logical circuits. Requires theory "WordBitwise" from HOL-Word 1.23 -session. Supports addition, subtraction, multiplication, shifting by 1.24 -constants, bitwise operators and numeric constants. Requires fixed-length word 1.25 -types, cannot operate on 'a word. Solves many standard word identies outright 1.26 -and converts more into first order problems amenable to blast or similar. See 1.27 -HOL/Word/WordBitwise.thy and examples in HOL/Word/Examples/WordExamples.thy. 1.28 +* New proof method "word_bitwise" for splitting machine word 1.29 +equalities and inequalities into logical circuits, defined in 1.30 +HOL/Word/WordBitwise.thy. Supports addition, subtraction, 1.31 +multiplication, shifting by constants, bitwise operators and numeric 1.32 +constants. Requires fixed-length word types, not 'a word. Solves 1.33 +many standard word identies outright and converts more into first 1.34 +order problems amenable to blast or similar. See also examples in 1.35 +HOL/Word/Examples/WordExamples.thy. 1.36 1.37 * Clarified attribute "mono_set": pure declaration without modifying 1.38 the result of the fact expression. 1.39 @@ -658,17 +658,18 @@ 1.40 1.41 * Theory Library/Multiset: Improved code generation of multisets. 1.42 1.43 -* Session HOL-Probability: Introduced the type "'a measure" to represent 1.44 -measures, this replaces the records 'a algebra and 'a measure_space. The 1.45 -locales based on subset_class now have two locale-parameters the space 1.46 -\<Omega> and the set of measurables sets M. The product of probability spaces 1.47 -uses now the same constant as the finite product of sigma-finite measure 1.48 -spaces "PiM :: ('i => 'a) measure". Most constants are defined now 1.49 -outside of locales and gain an additional parameter, like null_sets, 1.50 -almost_eventually or \<mu>'. Measure space constructions for distributions 1.51 -and densities now got their own constants distr and density. Instead of 1.52 -using locales to describe measure spaces with a finite space, the 1.53 -measure count_space and point_measure is introduced. INCOMPATIBILITY. 1.54 +* Session HOL-Probability: Introduced the type "'a measure" to 1.55 +represent measures, this replaces the records 'a algebra and 'a 1.56 +measure_space. The locales based on subset_class now have two 1.57 +locale-parameters the space \<Omega> and the set of measurables sets 1.58 +M. The product of probability spaces uses now the same constant as 1.59 +the finite product of sigma-finite measure spaces "PiM :: ('i => 'a) 1.60 +measure". Most constants are defined now outside of locales and gain 1.61 +an additional parameter, like null_sets, almost_eventually or \<mu>'. 1.62 +Measure space constructions for distributions and densities now got 1.63 +their own constants distr and density. Instead of using locales to 1.64 +describe measure spaces with a finite space, the measure count_space 1.65 +and point_measure is introduced. INCOMPATIBILITY. 1.66 1.67 Renamed constants: 1.68 measure -> emeasure 1.69 @@ -854,12 +855,12 @@ 1.70 replaced with corresponding ones according to the transfer rules. 1.71 Goals are generalized over all free variables by default; this is 1.72 necessary for variables whose types changes, but can be overridden 1.73 - for specific variables with e.g. 'transfer fixing: x y z'. 1.74 - The variant transfer' method allows replacing a subgoal with 1.75 - one that is logically stronger (rather than equivalent). 1.76 + for specific variables with e.g. 'transfer fixing: x y z'. The 1.77 + variant transfer' method allows replacing a subgoal with one that 1.78 + is logically stronger (rather than equivalent). 1.79 1.80 - relator_eq attribute: Collects identity laws for relators of 1.81 - various type constructors, e.g. "list_all2 (op =) = (op =)". The 1.82 + various type constructors, e.g. "list_all2 (op =) = (op =)". The 1.83 transfer method uses these lemmas to infer transfer rules for 1.84 non-polymorphic constants on the fly. 1.85 1.86 @@ -874,8 +875,8 @@ 1.87 * New Lifting package: 1.88 1.89 - lift_definition command: Defines operations on an abstract type in 1.90 - terms of a corresponding operation on a representation type. Example 1.91 - syntax: 1.92 + terms of a corresponding operation on a representation 1.93 + type. Example syntax: 1.94 1.95 lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" 1.96 is List.insert 1.97 @@ -892,11 +893,11 @@ 1.98 lift_definition generates a code certificate theorem and sets up 1.99 code generation for each constant. 1.100 1.101 - - setup_lifting command: Sets up the Lifting package to work with 1.102 - a user-defined type. The user must provide either a quotient 1.103 - theorem or a type_definition theorem. The package configures 1.104 - transfer rules for equality and quantifiers on the type, and sets 1.105 - up the lift_definition command to work with the type. 1.106 + - setup_lifting command: Sets up the Lifting package to work with a 1.107 + user-defined type. The user must provide either a quotient theorem 1.108 + or a type_definition theorem. The package configures transfer 1.109 + rules for equality and quantifiers on the type, and sets up the 1.110 + lift_definition command to work with the type. 1.111 1.112 - Usage examples: See Quotient_Examples/Lift_DList.thy, 1.113 Quotient_Examples/Lift_RBT.thy, Word/Word.thy and 1.114 @@ -957,11 +958,11 @@ 1.115 affecting 'rat' and 'real'. 1.116 1.117 * Sledgehammer: 1.118 - - Integrated more tightly with SPASS, as described in the ITP 2012 paper "More 1.119 - SPASS with Isabelle". 1.120 + - Integrated more tightly with SPASS, as described in the ITP 2012 1.121 + paper "More SPASS with Isabelle". 1.122 - Made it try "smt" as a fallback if "metis" fails or times out. 1.123 - - Added support for the following provers: Alt-Ergo (via Why3 and TFF1), 1.124 - iProver, iProver-Eq. 1.125 + - Added support for the following provers: Alt-Ergo (via Why3 and 1.126 + TFF1), iProver, iProver-Eq. 1.127 - Replaced remote E-SInE with remote Satallax in the default setup. 1.128 - Sped up the minimizer. 1.129 - Added "lam_trans", "uncurry_aliases", and "minimize" options. 1.130 @@ -1058,12 +1059,12 @@ 1.131 evaluated. Minor INCOMPATIBILITY: need to adapt Isabelle path where 1.132 the generic user home was intended. 1.133 1.134 +* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name 1.135 +notation, which is useful for the jEdit file browser, for example. 1.136 + 1.137 * ISABELLE_JDK_HOME settings variable points to JDK with javac and jar 1.138 (not just JRE). 1.139 1.140 -* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name 1.141 -notation, which is useful for the jEdit file browser, for example. 1.142 - 1.143 1.144 1.145 New in Isabelle2011-1 (October 2011)