Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recovered nat_induct as default for induct_tac;
authorwenzelm
Tue, 10 Jun 2008 21:50:05 +0200
changeset 27136 06a8f65e32f6
parent 27135 7fa9fa0bccee
child 27137 d0070c32fdc1
recovered nat_induct as default for induct_tac;
src/HOL/Word/WordGenLib.thy file | annotate | diff | comparison | revisions
src/HOL/Word/WordShift.thy file | annotate | diff | comparison | revisions 
--- 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)
--- 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
isabelle