author | wenzelm |

Sat Dec 29 18:34:42 2001 +0100 (2001-12-29) | |

changeset 12608 | 2df381faa787 |

parent 12607 | 16b63730cfbb |

child 12609 | fb073a34b537 |

* ZF/IMP: updated and converted to new-style theory format;

1.1 --- a/NEWS Sat Dec 29 13:14:11 2001 +0100 1.2 +++ b/NEWS Sat Dec 29 18:34:42 2001 +0100 1.3 @@ -143,7 +143,7 @@ 1.4 * HOL: properly declared induction rules less_induct and 1.5 wf_induct_rule; 1.6 1.7 -* HOLCF: domain package adapted to new-style theories, e.g. see 1.8 +* HOLCF: domain package adapted to new-style theory format, e.g. see 1.9 HOLCF/ex/Dnat.thy; 1.10 1.11 * ZF: proper integration of logic-specific tools and packages, 1.12 @@ -245,9 +245,9 @@ 1.13 * HOL/GroupTheory: group theory examples including Sylow's theorem (by 1.14 Florian Kammüller); 1.15 1.16 -* HOL/IMP: updated and converted to new-style theory; several parts 1.17 -turned into readable document, with proper Isar proof texts and some 1.18 -explanations (by Gerwin Klein); 1.19 +* HOL/IMP: updated and converted to new-style theory format; several 1.20 +parts turned into readable document, with proper Isar proof texts and 1.21 +some explanations (by Gerwin Klein); 1.22 1.23 1.24 *** HOLCF *** 1.25 @@ -267,8 +267,11 @@ 1.26 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a 1.27 typeless version of the formalism; 1.28 1.29 +* ZF/IMP: updated and converted to new-style theory format; 1.30 + 1.31 * ZF/Induct: new directory for examples of inductive definitions, 1.32 -including theory Multiset for multiset orderings; 1.33 +including theory Multiset for multiset orderings; converted to 1.34 +new-style theory format; 1.35 1.36 * ZF: the integer library now covers quotients and remainders, with 1.37 many laws relating division to addition, multiplication, etc.;