canonical 'cases'/'induct' rules for n-tuples (n=3..7)
authorkleing
Mon Oct 15 21:04:46 2001 +0200 (2001-10-15)
changeset 1178860054fee3c16
parent 11787 85b3735a51e1
child 11789 da81334357ba
canonical 'cases'/'induct' rules for n-tuples (n=3..7)
NEWS
     1.1 --- a/NEWS	Mon Oct 15 21:04:32 2001 +0200
     1.2 +++ b/NEWS	Mon Oct 15 21:04:46 2001 +0200
     1.3 @@ -40,6 +40,8 @@
     1.4  * HOL: 'inductive' now longer features separate (collective)
     1.5  attributes for 'intros';
     1.6  
     1.7 +* HOL: canonical 'cases'/'induct' rules for n-tuples (n=3..7)
     1.8 +
     1.9  
    1.10  *** HOL ***
    1.11