summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 20 Sep 2005 21:48:47 +0200 | |

changeset 17533 | f22f2ffd78ba |

parent 17532 | ab75f2b0cec6 |

child 17534 | 56e8db202f66 |

tuned;

--- a/NEWS Tue Sep 20 21:48:37 2005 +0200 +++ b/NEWS Tue Sep 20 21:48:47 2005 +0200 @@ -359,7 +359,9 @@ {)\([^\.]*\)\.\. -> {\1<\.\.} \.\.\([^(}]*\)(} -> \.\.<\1} -* Method comm_ring for proving equalities in commutative rings. +* Theory Commutative_Ring (in Library): method comm_ring for proving +equalities in commutative rings; method 'algebra' provides a generic +interface. * Theory Finite_Set: changed the syntax for 'setsum', summation over finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is @@ -642,30 +644,31 @@ *** HOLCF *** -* HOLCF: discontinued special version of 'constdefs' (which used to -support continuous functions) in favor of the general Pure one with -full type-inference. - -* HOLCF: new simplification procedure for solving continuity conditions; -it is much faster on terms with many nested lambda abstractions (cubic +* Discontinued special version of 'constdefs' (which used to support +continuous functions) in favor of the general Pure one with full +type-inference. + +* New simplification procedure for solving continuity conditions; it +is much faster on terms with many nested lambda abstractions (cubic instead of exponential time). -* HOLCF: new syntax for domain package: selector names are now optional. +* New syntax for domain package: selector names are now optional. Parentheses should be omitted unless argument is lazy, for example: domain 'a stream = cons "'a" (lazy "'a stream") -* HOLCF: new command "fixrec" for defining recursive functions with pattern -matching; defining multiple functions with mutual recursion is also supported. -Patterns may include the constants cpair, spair, up, sinl, sinr, or any data -constructor defined by the domain package. The given equations are proven as -rewrite rules. See HOLCF/ex/Fixrec_ex.thy for syntax and examples. - -* HOLCF: new commands "cpodef" and "pcpodef" for defining predicate subtypes -of cpo and pcpo types. Syntax is exactly like the "typedef" command, but the -proof obligation additionally includes an admissibility requirement. The -packages generate instances of class cpo or pcpo, with continuity and -strictness theorems for Rep and Abs. +* New command 'fixrec' for defining recursive functions with pattern +matching; defining multiple functions with mutual recursion is also +supported. Patterns may include the constants cpair, spair, up, sinl, +sinr, or any data constructor defined by the domain package. The given +equations are proven as rewrite rules. See HOLCF/ex/Fixrec_ex.thy for +syntax and examples. + +* New commands 'cpodef' and 'pcpodef' for defining predicate subtypes +of cpo and pcpo types. Syntax is exactly like the 'typedef' command, +but the proof obligation additionally includes an admissibility +requirement. The packages generate instances of class cpo or pcpo, +with continuity and strictness theorems for Rep and Abs. *** ZF ***