strengthened lemma
authornipkow
Tue May 21 11:47:11 2019 +0200 (5 weeks ago ago)
changeset 7046091a2f79b546b
parent 70458 7daa65d45462
child 70461 910dc065b869
strengthened lemma
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Mon May 20 17:33:13 2019 +0200
     1.2 +++ b/src/HOL/List.thy	Tue May 21 11:47:11 2019 +0200
     1.3 @@ -791,7 +791,7 @@
     1.4  by (fact measure_induct)
     1.5  
     1.6  lemma induct_list012:
     1.7 -  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
     1.8 +  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. \<lbrakk> P zs; P (y # zs) \<rbrakk> \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
     1.9  by induction_schema (pat_completeness, lexicographic_order)
    1.10  
    1.11  lemma list_nonempty_induct [consumes 1, case_names single cons]: