# HG changeset patch
# User desharna
# Date 1615287021 -3600
# Node ID d47c8a89c6a57a6f54bc686b62f139483782e65f
# Parent  8a1c6c7909c991c61290ce2f4464230c9ad226ca
Backed out changeset 3fdb94d87e0e

diff -r 8a1c6c7909c9 -r d47c8a89c6a5 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Tue Mar 09 11:50:11 2021 +0100
+++ b/src/HOL/Library/Sublist.thy	Tue Mar 09 11:50:21 2021 +0100
@@ -1385,12 +1385,6 @@
     by (simp add: ys zs1 zs2)
 qed
 
-lemma sublist_list_all: "sublist xs ys \<Longrightarrow> list_all P ys \<Longrightarrow> list_all P xs"
-  by (auto simp: sublist_def)
-
-lemmas prefix_list_all = prefix_imp_sublist[THEN sublist_list_all]
-lemmas suffix_list_all = suffix_imp_sublist[THEN sublist_list_all]
-
 subsubsection \<open>\<open>sublists\<close>\<close>
 
 primrec sublists :: "'a list \<Rightarrow> 'a list list" where