author | wenzelm |

Thu Jan 03 17:50:53 2002 +0100 (2002-01-03) | |

changeset 12622 | 7592926925d4 |

parent 12621 | 48cafea0684b |

child 12623 | 7a33541fd81b |

tuned;

1.1 --- a/NEWS Thu Jan 03 17:48:02 2002 +0100 1.2 +++ b/NEWS Thu Jan 03 17:50:53 2002 +0100 1.3 @@ -143,14 +143,6 @@ 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 theory format, e.g. see 1.8 -HOLCF/ex/Dnat.thy; 1.9 - 1.10 -* ZF: proper integration of logic-specific tools and packages, 1.11 -including theory commands '(co)inductive', '(co)datatype', 1.12 -'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', 1.13 -'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); 1.14 - 1.15 1.16 *** HOL *** 1.17 1.18 @@ -252,7 +244,13 @@ 1.19 1.20 *** HOLCF *** 1.21 1.22 -* proper rep_datatype lift (see theory Lift) instead of ML hacks -- 1.23 +* Isar: consts/constdefs supports mixfix syntax for continuous 1.24 +operations; 1.25 + 1.26 +* Isar: domain package adapted to new-style theory format, e.g. see 1.27 +HOLCF/ex/Dnat.thy; 1.28 + 1.29 +* theory Lift: proper use of rep_datatype lift instead of ML hacks -- 1.30 potential INCOMPATIBILITY; now use plain induct_tac instead of former 1.31 lift.induct_tac, always use UU instead of Undef; 1.32 1.33 @@ -261,8 +259,16 @@ 1.34 1.35 *** ZF *** 1.36 1.37 -* Theory Main no longer includes AC; for the Axiom of Choice, base your 1.38 -theory on Main_ZFC; 1.39 +* Isar: proper integration of logic-specific tools and packages, 1.40 +including theory commands '(co)inductive', '(co)datatype', 1.41 +'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', 1.42 +'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); 1.43 + 1.44 +* theory Main no longer includes AC; for the Axiom of Choice, base 1.45 +your theory on Main_ZFC; 1.46 + 1.47 +* the integer library now covers quotients and remainders, with many 1.48 +laws relating division to addition, multiplication, etc.; 1.49 1.50 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a 1.51 typeless version of the formalism; 1.52 @@ -273,9 +279,6 @@ 1.53 including theory Multiset for multiset orderings; converted to 1.54 new-style theory format; 1.55 1.56 -* ZF: the integer library now covers quotients and remainders, with 1.57 -many laws relating division to addition, multiplication, etc.; 1.58 - 1.59 1.60 *** General *** 1.61 1.62 @@ -356,7 +359,7 @@ 1.63 1.64 * HOL: please note that theories in the Library and elsewhere often use the 1.65 new-style (Isar) format; to refer to their theorems in an ML script you must 1.66 -bind them to ML identifers by e.g. val thm_name = thm "thm_name"; 1.67 +bind them to ML identifers by e.g. val thm_name = thm "thm_name"; 1.68 1.69 * HOL: inductive package no longer splits induction rule aggressively, 1.70 but only as far as specified by the introductions given; the old