tuned;
authorwenzelm
Tue Sep 20 21:48:47 2005 +0200 (2005-09-20)
changeset 17533f22f2ffd78ba
parent 17532 ab75f2b0cec6
child 17534 56e8db202f66
tuned;
NEWS
     1.1 --- a/NEWS	Tue Sep 20 21:48:37 2005 +0200
     1.2 +++ b/NEWS	Tue Sep 20 21:48:47 2005 +0200
     1.3 @@ -359,7 +359,9 @@
     1.4    {)\([^\.]*\)\.\.  ->  {\1<\.\.}
     1.5    \.\.\([^(}]*\)(}  ->  \.\.<\1}
     1.6  
     1.7 -* Method comm_ring for proving equalities in commutative rings.
     1.8 +* Theory Commutative_Ring (in Library): method comm_ring for proving
     1.9 +equalities in commutative rings; method 'algebra' provides a generic
    1.10 +interface.
    1.11  
    1.12  * Theory Finite_Set: changed the syntax for 'setsum', summation over
    1.13  finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
    1.14 @@ -642,30 +644,31 @@
    1.15  
    1.16  *** HOLCF ***
    1.17  
    1.18 -* HOLCF: discontinued special version of 'constdefs' (which used to
    1.19 -support continuous functions) in favor of the general Pure one with
    1.20 -full type-inference.
    1.21 -
    1.22 -* HOLCF: new simplification procedure for solving continuity conditions;
    1.23 -it is much faster on terms with many nested lambda abstractions (cubic
    1.24 +* Discontinued special version of 'constdefs' (which used to support
    1.25 +continuous functions) in favor of the general Pure one with full
    1.26 +type-inference.
    1.27 +
    1.28 +* New simplification procedure for solving continuity conditions; it
    1.29 +is much faster on terms with many nested lambda abstractions (cubic
    1.30  instead of exponential time).
    1.31  
    1.32 -* HOLCF: new syntax for domain package: selector names are now optional.
    1.33 +* New syntax for domain package: selector names are now optional.
    1.34  Parentheses should be omitted unless argument is lazy, for example:
    1.35  
    1.36    domain 'a stream = cons "'a" (lazy "'a stream")
    1.37  
    1.38 -* HOLCF: new command "fixrec" for defining recursive functions with pattern
    1.39 -matching; defining multiple functions with mutual recursion is also supported.
    1.40 -Patterns may include the constants cpair, spair, up, sinl, sinr, or any data
    1.41 -constructor defined by the domain package. The given equations are proven as
    1.42 -rewrite rules. See HOLCF/ex/Fixrec_ex.thy for syntax and examples.
    1.43 -
    1.44 -* HOLCF: new commands "cpodef" and "pcpodef" for defining predicate subtypes
    1.45 -of cpo and pcpo types. Syntax is exactly like the "typedef" command, but the
    1.46 -proof obligation additionally includes an admissibility requirement. The
    1.47 -packages generate instances of class cpo or pcpo, with continuity and
    1.48 -strictness theorems for Rep and Abs.
    1.49 +* New command 'fixrec' for defining recursive functions with pattern
    1.50 +matching; defining multiple functions with mutual recursion is also
    1.51 +supported.  Patterns may include the constants cpair, spair, up, sinl,
    1.52 +sinr, or any data constructor defined by the domain package. The given
    1.53 +equations are proven as rewrite rules. See HOLCF/ex/Fixrec_ex.thy for
    1.54 +syntax and examples.
    1.55 +
    1.56 +* New commands 'cpodef' and 'pcpodef' for defining predicate subtypes
    1.57 +of cpo and pcpo types. Syntax is exactly like the 'typedef' command,
    1.58 +but the proof obligation additionally includes an admissibility
    1.59 +requirement. The packages generate instances of class cpo or pcpo,
    1.60 +with continuity and strictness theorems for Rep and Abs.
    1.61  
    1.62  
    1.63  *** ZF ***