# HG changeset patch
# User nipkow
# Date 1558432031 -7200
# Node ID 91a2f79b546becad42423e6bcfb2db99db0d40d5
# Parent  7daa65d45462d6728a62633168e0eece41068c60
strengthened lemma

diff -r 7daa65d45462 -r 91a2f79b546b src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 20 17:33:13 2019 +0200
+++ b/src/HOL/List.thy	Tue May 21 11:47:11 2019 +0200
@@ -791,7 +791,7 @@
 by (fact measure_induct)
 
 lemma induct_list012:
-  "\<lbrakk>P []; \<And>x. P [x]; \<And>x y zs. P (y # zs) \<Longrightarrow> P (x # y # zs)\<rbrakk> \<Longrightarrow> P xs"
+  "\<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"
 by induction_schema (pat_completeness, lexicographic_order)
 
 lemma list_nonempty_induct [consumes 1, case_names single cons]: