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

author | wenzelm |

Tue, 04 Nov 1997 16:21:52 +0100 | |

changeset 4125 | dc1cf9db1e17 |

parent 4124 | 1af16493c57f |

child 4126 | c41846a38e20 |

tuned;

--- a/NEWS Tue Nov 04 16:17:04 1997 +0100 +++ b/NEWS Tue Nov 04 16:21:52 1997 +0100 @@ -91,7 +91,7 @@ * HOL/Auth: new protocol proofs including some for the Internet protocol TLS; -* HOL/Map: new theory of `maps' a la VDM. +* HOL/Map: new theory of `maps' a la VDM; * HOL/simplifier: added infix function `addsplits': instead of `<simpset> setloop (split_tac <thms>)' @@ -122,20 +122,23 @@ * HOL/Lists: the function "set_of_list" has been renamed "set" (and its theorems too); + *** HOLCF *** -* removed "axioms" and "generated by" section +* removed "axioms" and "generated by" sections; + * replaced "ops" section by extended "consts" section, which is capable of - handling the continuous function space "->" directly -* domain package: proves theorems immediately and stores them in the theory - creates hierachical name space - now uses normal mixfix annotations (instead of cinfix...) - minor changes to some names and values (for consistency), - e.g. cases -> casedist, dists_eq -> dist_eqs, - [take_lemma] -> take_lemmas - separator between mutual domain defs: changed "," to "and" - improved handling of sort constraints. Now they have to - appear on the left-hand side of the equations only. + handling the continuous function space "->" directly; + +* domain package: + . proves theorems immediately and stores them in the theory, + . creates hierachical name space, + . now uses normal mixfix annotations (instead of cinfix...), + . minor changes to some names and values (for consistency), + . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas, + . separator between mutual domain defs: changed "," to "and", + . improved handling of sort constraints; now they have to + appear on the left-hand side of the equations only; * fixed LAM <x,y,zs>.b syntax;