drop a superfluous assumption that was found by the find_unused_assms command and tune proof
--- a/src/HOL/List.thy Fri Oct 20 20:57:55 2017 +0200
+++ b/src/HOL/List.thy Sat Oct 21 18:11:29 2017 +0200
@@ -4902,9 +4902,8 @@
by(induction xs arbitrary: x)(auto intro: transpD[OF assms])
lemma sorted_wrt_ConsI:
- "\<lbrakk> transp P; \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow>
- sorted_wrt P (x # xs)"
-by (simp add: sorted_wrt_Cons)
+ "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)"
+by (induction xs rule: sorted_wrt_induct) simp_all
lemma sorted_wrt_append:
assumes "transp P"