src/HOL/List.thy
changeset 70460 91a2f79b546b
parent 70410 accbd801fefa
child 70481 8dd987397e31
     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]: