| changeset 3316 | c2e9ab7d2724 |
| parent 3227 | 9190438471ea |
| child 3317 | 2cfb98c49c42 |
--- a/NEWS Fri May 23 14:13:51 1997 +0200 +++ b/NEWS Fri May 23 14:17:40 1997 +0200 @@ -94,6 +94,11 @@ * a generic induction tactic `induct_tac' which works for all datatypes and also for type `nat'; +* a generic case distinction tactic `exhaust_tac' which works for all +datatypes and also for type `nat'; + +* each datatype comes with a function `size'; + * patterns in case expressions allow tuple patterns as arguments to constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';