# HG changeset patch
# User wenzelm
# Date 1213127405 -7200
# Node ID 06a8f65e32f66351811b21822aa0263fbc08eee7
# Parent  7fa9fa0bcceeb60840741b4bfb70788e0f5a8ab2
recovered nat_induct as default for induct_tac;

diff -r 7fa9fa0bccee -r 06a8f65e32f6 src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Tue Jun 10 21:49:37 2008 +0200
+++ b/src/HOL/Word/WordGenLib.thy	Tue Jun 10 21:50:05 2008 +0200
@@ -318,7 +318,7 @@
   apply atomize
   apply (erule rev_mp)+
   apply (rule_tac x=m in spec)
-  apply (induct_tac n rule: nat_induct)
+  apply (induct_tac n)
    apply simp
   apply clarsimp
   apply (erule impE)
diff -r 7fa9fa0bccee -r 06a8f65e32f6 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Tue Jun 10 21:49:37 2008 +0200
+++ b/src/HOL/Word/WordShift.thy	Tue Jun 10 21:50:05 2008 +0200
@@ -121,12 +121,12 @@
        apply arith
       apply arith
      apply (erule thin_rl)
-     apply (case_tac nat)
+     apply (case_tac n)
       apply safe
       apply simp
      apply simp
     apply (erule thin_rl)
-    apply (case_tac nat)
+    apply (case_tac n)
      apply safe
      apply simp
     apply simp