NEWS
changeset 32774 461afcc6acb8
parent 32706 b68f3afdc137
child 32775 d498770eefdc
     1.1 --- a/NEWS	Wed Sep 30 08:22:07 2009 +0200
     1.2 +++ b/NEWS	Wed Sep 30 08:28:23 2009 +0200
     1.3 @@ -18,6 +18,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Most rules produced by inductive and datatype package
     1.8 +have mandatory prefixes.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * New proof method "smt" for a combination of first-order logic
    1.12  with equality, linear and nonlinear (natural/integer/real)
    1.13  arithmetic, and fixed-size bitvectors; there is also basic