author | wenzelm |

Tue Sep 20 21:48:47 2005 +0200 (2005-09-20) | |

changeset 17533 | f22f2ffd78ba |

parent 17532 | ab75f2b0cec6 |

child 17534 | 56e8db202f66 |

tuned;

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 ***