final tuning; Isabelle2009-2
authorwenzelm
Mon Jun 21 11:24:19 2010 +0200 (2010-06-21)
changeset 3738035815ce9218a
parent 37379 f23e60581eb3
child 37381 5a8981a7acbc
final tuning;
NEWS
     1.1 --- a/NEWS	Mon Jun 14 10:38:28 2010 +0200
     1.2 +++ b/NEWS	Mon Jun 21 11:24:19 2010 +0200
     1.3 @@ -160,15 +160,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 @@ -250,6 +250,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 @@ -3386,8 +3388,6 @@
    1.33  * Real: proper support for ML code generation, including 'quickcheck'.
    1.34  Reals are implemented as arbitrary precision rationals.
    1.35  
    1.36 -* Real: new development using Cauchy Sequences.
    1.37 -
    1.38  * Hyperreal: Several constants that previously worked only for the
    1.39  reals have been generalized, so they now work over arbitrary vector
    1.40  spaces. Type annotations may need to be added in some cases; potential