src/HOL/Word/WordGenLib.thy
changeset 27133 e26ed41cc8ea
parent 26558 7fcc10088e72
child 27136 06a8f65e32f6
equal deleted inserted replaced
27132:7d643d3935b1 27133:e26ed41cc8ea
   316   "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
   316   "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
   317   apply (cases m)
   317   apply (cases m)
   318   apply atomize
   318   apply atomize
   319   apply (erule rev_mp)+
   319   apply (erule rev_mp)+
   320   apply (rule_tac x=m in spec)
   320   apply (rule_tac x=m in spec)
   321   apply (induct_tac n)
   321   apply (induct_tac n rule: nat_induct)
   322    apply simp
   322    apply simp
   323   apply clarsimp
   323   apply clarsimp
   324   apply (erule impE)
   324   apply (erule impE)
   325    apply clarsimp
   325    apply clarsimp
   326    apply (erule_tac x=n in allE)
   326    apply (erule_tac x=n in allE)