induct_tac
authornipkow
Thu, 24 Apr 1997 18:38:30 +0200
changeset 3042 21cd332b65d3
parent 3041 bdd21deed6ea
child 3043 63a77d6b7eca
induct_tac
NEWS
--- 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 => ...'