| author | nipkow |
| Thu, 24 Apr 1997 18:38:30 +0200 | |
| changeset 3042 | 21cd332b65d3 |
| parent 3041 | bdd21deed6ea |
| child 3043 | 63a77d6b7eca |
--- a/NEWS Thu Apr 24 18:07:35 1997 +0200 +++ b/NEWS Thu Apr 24 18:38:30 1997 +0200 @@ -86,6 +86,9 @@ *** HOL *** +* a generic induction tactic `induct_tac' which works for all datatypes and +also for type `nat'. + * patterns in case expressions allow tuple patterns as arguments to constructors, for example `case x of [] => ... | (x,y,z)#ps => ...'