# HG changeset patch # User wenzelm # Date 1010076653 -3600 # Node ID 7592926925d4496cc584549ecff03771218a9397 # Parent 48cafea0684b4a34227d6758fe01fa2ab409b295 tuned; diff -r 48cafea0684b -r 7592926925d4 NEWS --- a/NEWS Thu Jan 03 17:48:02 2002 +0100 +++ b/NEWS Thu Jan 03 17:50:53 2002 +0100 @@ -143,14 +143,6 @@ * HOL: properly declared induction rules less_induct and wf_induct_rule; -* HOLCF: domain package adapted to new-style theory format, e.g. see -HOLCF/ex/Dnat.thy; - -* ZF: proper integration of logic-specific tools and packages, -including theory commands '(co)inductive', '(co)datatype', -'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', -'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); - *** HOL *** @@ -252,7 +244,13 @@ *** HOLCF *** -* proper rep_datatype lift (see theory Lift) instead of ML hacks -- +* Isar: consts/constdefs supports mixfix syntax for continuous +operations; + +* Isar: domain package adapted to new-style theory format, e.g. see +HOLCF/ex/Dnat.thy; + +* theory Lift: proper use of rep_datatype lift instead of ML hacks -- potential INCOMPATIBILITY; now use plain induct_tac instead of former lift.induct_tac, always use UU instead of Undef; @@ -261,8 +259,16 @@ *** ZF *** -* Theory Main no longer includes AC; for the Axiom of Choice, base your -theory on Main_ZFC; +* Isar: proper integration of logic-specific tools and packages, +including theory commands '(co)inductive', '(co)datatype', +'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', +'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); + +* theory Main no longer includes AC; for the Axiom of Choice, base +your theory on Main_ZFC; + +* the integer library now covers quotients and remainders, with many +laws relating division to addition, multiplication, etc.; * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless version of the formalism; @@ -273,9 +279,6 @@ including theory Multiset for multiset orderings; converted to new-style theory format; -* ZF: the integer library now covers quotients and remainders, with -many laws relating division to addition, multiplication, etc.; - *** General *** @@ -356,7 +359,7 @@ * HOL: please note that theories in the Library and elsewhere often use the new-style (Isar) format; to refer to their theorems in an ML script you must -bind them to ML identifers by e.g. val thm_name = thm "thm_name"; +bind them to ML identifers by e.g. val thm_name = thm "thm_name"; * HOL: inductive package no longer splits induction rule aggressively, but only as far as specified by the introductions given; the old