--- a/NEWS Mon Jun 21 16:59:37 2010 +0200
+++ b/NEWS Mon Jun 21 17:41:57 2010 +0200
@@ -202,15 +202,15 @@
'quotient_definition' may be used for defining types and constants by
quotient constructions. An example is the type of integers created by
quotienting pairs of natural numbers:
-
+
fun
- intrel :: "(nat * nat) => (nat * nat) => bool"
+ intrel :: "(nat * nat) => (nat * nat) => bool"
where
"intrel (x, y) (u, v) = (x + v = u + y)"
- quotient_type int = "nat × nat" / intrel
+ quotient_type int = "nat * nat" / intrel
by (auto simp add: equivp_def expand_fun_eq)
-
+
quotient_definition
"0::int" is "(0::nat, 0::nat)"
@@ -292,6 +292,8 @@
* Theory PReal, including the type "preal" and related operations, has
been removed. INCOMPATIBILITY.
+* Real: new development using Cauchy Sequences.
+
* Split off theory "Big_Operators" containing setsum, setprod,
Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
@@ -511,6 +513,17 @@
"sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
- Removed "nitpick_intro" attribute. INCOMPATIBILITY.
+* Method "induct" now takes instantiations of the form t, where t is not
+ a variable, as a shorthand for "x == t", where x is a fresh variable.
+ If this is not intended, t has to be enclosed in parentheses.
+ By default, the equalities generated by definitional instantiations
+ are pre-simplified, which may cause parameters of inductive cases
+ to disappear, or may even delete some of the inductive cases.
+ Use "induct (no_simp)" instead of "induct" to restore the old
+ behaviour. The (no_simp) option is also understood by the "cases"
+ and "nominal_induct" methods, which now perform pre-simplification, too.
+ INCOMPATIBILITY.
+
*** HOLCF ***
@@ -683,6 +696,13 @@
See src/Tools/jEdit or "isabelle jedit" provided by the properly built
component.
+* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
+and Bluesky TeX fonts. It provides the usual Isabelle symbols,
+similar to the default assignment of the document preparation system
+(cf. isabellesym.sty). The Isabelle/Scala class Isabelle_System
+provides some operations for direct access to the font without asking
+the user for manual installation.
+
New in Isabelle2009-1 (December 2009)
@@ -3410,8 +3430,6 @@
* Real: proper support for ML code generation, including 'quickcheck'.
Reals are implemented as arbitrary precision rationals.
-* Real: new development using Cauchy Sequences.
-
* Hyperreal: Several constants that previously worked only for the
reals have been generalized, so they now work over arbitrary vector
spaces. Type annotations may need to be added in some cases; potential