--- a/NEWS Sat Feb 28 17:09:32 2009 +0100
+++ b/NEWS Sat Feb 28 10:55:10 2009 -0800
@@ -246,7 +246,7 @@
src/HOL/Library/Order_Relation.thy ~> src/HOL/
src/HOL/Library/Parity.thy ~> src/HOL/
src/HOL/Library/Univ_Poly.thy ~> src/HOL/
- src/HOL/Real/ContNotDenum.thy ~> src/HOL/
+ src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/
src/HOL/Real/Lubs.thy ~> src/HOL/
src/HOL/Real/PReal.thy ~> src/HOL/
src/HOL/Real/Rational.thy ~> src/HOL/
@@ -256,8 +256,8 @@
src/HOL/Real/Real.thy ~> src/HOL/
src/HOL/Complex/Complex_Main.thy ~> src/HOL/
src/HOL/Complex/Complex.thy ~> src/HOL/
- src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/
- src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/
+ src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/
+ src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/
src/HOL/Hyperreal/Deriv.thy ~> src/HOL/
src/HOL/Hyperreal/Fact.thy ~> src/HOL/
src/HOL/Hyperreal/Integration.thy ~> src/HOL/
@@ -420,7 +420,7 @@
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd,
zlcm (for int); carried together from various gcd/lcm developements in
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm;
-corresponding theorems renamed accordingly. INCOMPATIBILY. To
+corresponding theorems renamed accordingly. INCOMPATIBILITY. To
recover tupled syntax, use syntax declarations like:
hide (open) const gcd
@@ -434,7 +434,7 @@
* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY.
* The real numbers offer decimal input syntax: 12.34 is translated into
- 1234/10^4. This translation is not reversed upon output.
+ 1234/10^2. This translation is not reversed upon output.
* New ML antiquotation @{code}: takes constant as argument, generates
corresponding code in background and inserts name of the corresponding
@@ -534,6 +534,23 @@
* Proof of Zorn's Lemma for partial orders.
+*** HOLCF ***
+
+* Reimplemented the simplification procedure for proving continuity
+subgoals. The new simproc is extensible; users can declare additional
+continuity introduction rules with the attribute [cont2cont].
+
+* The continuity simproc now uses a different introduction rule for
+solving continuity subgoals on terms with lambda abstractions. In
+some rare cases the new simproc may fail to solve subgoals that the
+old one could solve, and "simp add: cont2cont_LAM" may be necessary.
+Potential INCOMPATIBILITY.
+
+* The syntax of the fixrec package has changed. The specification
+syntax now conforms in style to definition, primrec, function, etc.
+See HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY.
+
+
*** ML ***
* High-level support for concurrent ML programming, see