NEWS
 changeset 47807 befe55c8bbdc parent 47806 7e009f4e9f47 child 47809 4d8cbea248b0
```--- 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
+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
+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
-\<Omega> 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 \<mu>'. 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 \<Omega> 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 \<mu>'.
+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)```