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.
adhoc fix of induct_tac: rule nat_induct;
authorwenzelm
Tue, 10 Jun 2008 19:45:53 +0200
changeset 27133 e26ed41cc8ea
parent 27132 7d643d3935b1
child 27134 71461c77a15b
adhoc fix of induct_tac: rule nat_induct;
src/HOL/Word/WordGenLib.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle