NEWS
changeset 10915 6b66a8a530ce
parent 10868 5af3906edec8
child 10944 710ddb9e8b5e
     1.1 --- a/NEWS	Tue Jan 16 00:35:50 2001 +0100
     1.2 +++ b/NEWS	Tue Jan 16 00:37:41 2001 +0100
     1.3 @@ -106,6 +106,16 @@
     1.4  * HOL/typedef: simplified package, provide more useful rules (see also
     1.5  HOL/subset.thy);
     1.6  
     1.7 +* HOL/datatype: induction rule for arbitrarily branching datatypes is
     1.8 +now expressed as a proper nested rule (old-style tactic scripts may
     1.9 +require atomize_strip_tac to cope with non-atomic premises);
    1.10 +
    1.11 +* HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
    1.12 +to "split_conv" (old name still available for compatibility);
    1.13 +
    1.14 +* HOL: improved concrete syntax for strings (e.g. allows translation
    1.15 +rules with string literals);
    1.16 +
    1.17  * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and 
    1.18  Fleuriot's mechanization of analysis;
    1.19