1.1 --- a/NEWS	Mon Jun 21 16:59:37 2010 +0200
     1.2 +++ b/NEWS	Mon Jun 21 17:41:57 2010 +0200
     1.3 @@ -202,15 +202,15 @@
     1.4  'quotient_definition' may be used for defining types and constants by
     1.5  quotient constructions.  An example is the type of integers created by
     1.6  quotienting pairs of natural numbers:
     1.7 -  
     1.8 +
     1.9    fun
    1.10 -    intrel :: "(nat * nat) => (nat * nat) => bool" 
    1.11 +    intrel :: "(nat * nat) => (nat * nat) => bool"
    1.12    where
    1.13      "intrel (x, y) (u, v) = (x + v = u + y)"
    1.14  
    1.15 -  quotient_type int = "nat × nat" / intrel
    1.16 +  quotient_type int = "nat * nat" / intrel
    1.17      by (auto simp add: equivp_def expand_fun_eq)
    1.18 -  
    1.19 +
    1.20    quotient_definition
    1.21      "0::int" is "(0::nat, 0::nat)"
    1.22  
    1.23 @@ -292,6 +292,8 @@
    1.24  * Theory PReal, including the type "preal" and related operations, has
    1.25  been removed.  INCOMPATIBILITY.
    1.26  
    1.27 +* Real: new development using Cauchy Sequences.
    1.28 +
    1.29  * Split off theory "Big_Operators" containing setsum, setprod,
    1.30  Inf_fin, Sup_fin, Min, Max from theory Finite_Set.  INCOMPATIBILITY.
    1.31  
    1.32 @@ -511,6 +513,17 @@
    1.33      "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
    1.34    - Removed "nitpick_intro" attribute.  INCOMPATIBILITY.
    1.35  
    1.36 +* Method "induct" now takes instantiations of the form t, where t is not
    1.37 +  a variable, as a shorthand for "x == t", where x is a fresh variable.
    1.38 +  If this is not intended, t has to be enclosed in parentheses.
    1.39 +  By default, the equalities generated by definitional instantiations
    1.40 +  are pre-simplified, which may cause parameters of inductive cases
    1.41 +  to disappear, or may even delete some of the inductive cases.
    1.42 +  Use "induct (no_simp)" instead of "induct" to restore the old
    1.43 +  behaviour. The (no_simp) option is also understood by the "cases"
    1.44 +  and "nominal_induct" methods, which now perform pre-simplification, too.
    1.45 +  INCOMPATIBILITY.
    1.46 +
    1.47  
    1.48  *** HOLCF ***
    1.49  
    1.50 @@ -683,6 +696,13 @@
    1.51  See src/Tools/jEdit or "isabelle jedit" provided by the properly built
    1.52  component.
    1.53  
    1.54 +* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
    1.55 +and Bluesky TeX fonts.  It provides the usual Isabelle symbols,
    1.56 +similar to the default assignment of the document preparation system
    1.57 +(cf. isabellesym.sty).  The Isabelle/Scala class Isabelle_System
    1.58 +provides some operations for direct access to the font without asking
    1.59 +the user for manual installation.
    1.60 +
    1.61  
    1.62  
    1.63  New in Isabelle2009-1 (December 2009)
    1.64 @@ -3410,8 +3430,6 @@
    1.65  * Real: proper support for ML code generation, including 'quickcheck'.
    1.66  Reals are implemented as arbitrary precision rationals.
    1.67  
    1.68 -* Real: new development using Cauchy Sequences.
    1.69 -
    1.70  * Hyperreal: Several constants that previously worked only for the
    1.71  reals have been generalized, so they now work over arbitrary vector
    1.72  spaces. Type annotations may need to be added in some cases; potential