# HG changeset patch
# User desharna
# Date 1615287011 -3600
# Node ID 8a1c6c7909c991c61290ce2f4464230c9ad226ca
# Parent  6a96e9406e5349f17e1f2cfcd07192c109cd50ae
Backed out changeset b867b436f372

diff -r 6a96e9406e53 -r 8a1c6c7909c9 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Mar 07 08:26:02 2021 +0100
+++ b/src/HOL/List.thy	Tue Mar 09 11:50:11 2021 +0100
@@ -2386,21 +2386,6 @@
 lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
   by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
 
-lemma list_all_take_drop_conv:
-  "list_all P (take n xs) \<and> list_all P (drop n xs) \<longleftrightarrow> list_all P xs"
-proof (induction xs arbitrary: n)
-  case Nil
-  then show ?case by simp
-next
-  case (Cons a xs)
-  then show ?case
-    by (cases n) simp_all
-qed
-
-lemmas list_all_takeI = list_all_take_drop_conv[THEN iffD2, THEN conjunct1]
-lemmas list_all_dropI = list_all_take_drop_conv[THEN iffD2, THEN conjunct2]
-lemmas list_all_take_dropD = conjI[THEN list_all_take_drop_conv[THEN iffD1]]
-
 
 subsubsection \<open>\<^const>\<open>takeWhile\<close> and \<^const>\<open>dropWhile\<close>\<close>
 
@@ -2589,14 +2574,6 @@
   "dropWhile P (dropWhile P xs) = dropWhile P xs"
   by (induct xs) auto
 
-lemma list_all_takeWhile_dropWhile_conv:
-  "list_all P (takeWhile Q xs) \<and> list_all P (dropWhile Q xs) \<longleftrightarrow> list_all P xs"
-  by (induction xs; simp)
-
-lemmas list_all_takeWhileI = list_all_takeWhile_dropWhile_conv[THEN iffD2, THEN conjunct1]
-lemmas list_all_dropWhileI = list_all_takeWhile_dropWhile_conv[THEN iffD2, THEN conjunct2]
-lemmas list_all_takeWhile_dropWhileD = conjI[THEN list_all_takeWhile_dropWhile_conv[THEN iffD1]]
-
 
 subsubsection \<open>\<^const>\<open>zip\<close>\<close>