Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Word/WordGenLib.thy
changeset 27133 e26ed41cc8ea
parent 26558 7fcc10088e72
child 27136 06a8f65e32f6 
--- 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