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)