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 27136 06a8f65e32f6
parent 27133 e26ed41cc8ea
child 29235 2d62b637fa80 
--- 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)
isabelle