equal
deleted
inserted
replaced
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 rule: nat_induct) |
321 apply (induct_tac n) |
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) |