# HG changeset patch
# User wenzelm
# Date 1213119953 -7200
# Node ID e26ed41cc8eab525a7738bc26e399da066c178ee
# Parent  7d643d3935b1c8857b55f9af1651b1f327421295
adhoc fix of induct_tac: rule nat_induct;

diff -r 7d643d3935b1 -r e26ed41cc8ea src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Tue Jun 10 19:34:32 2008 +0200
+++ b/src/HOL/Word/WordGenLib.thy	Tue Jun 10 19:45:53 2008 +0200
@@ -318,7 +318,7 @@
   apply atomize
   apply (erule rev_mp)+
   apply (rule_tac x=m in spec)
-  apply (induct_tac n)
+  apply (induct_tac n rule: nat_induct)
    apply simp
   apply clarsimp
   apply (erule impE)