# HG changeset patch
# User haftmann
# Date 1457609581 -3600
# Node ID 7011429f44f98e4048e70ef71d785f3057f37ceb
# Parent  bfa38c2e751fd25e8097c28f7b8ff3b311ebfeae
moved

diff -r bfa38c2e751f -r 7011429f44f9 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Mar 09 21:01:22 2016 +0100
+++ b/src/HOL/List.thy	Thu Mar 10 12:33:01 2016 +0100
@@ -3006,6 +3006,14 @@
 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
 by (simp add: upt_rec)
 
+lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close>
+  "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
+proof (cases "m < q")
+  case False then show ?thesis by simp
+next
+  case True then show ?thesis by (simp add: upt_conv_Cons)
+qed
+
 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
 \<comment> \<open>LOOPS as a simprule, since \<open>j <= j\<close>.\<close>
 by (induct k) auto
diff -r bfa38c2e751f -r 7011429f44f9 src/HOL/String.thy
--- a/src/HOL/String.thy	Wed Mar 09 21:01:22 2016 +0100
+++ b/src/HOL/String.thy	Thu Mar 10 12:33:01 2016 +0100
@@ -6,15 +6,6 @@
 imports Enum
 begin
 
-lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close> -- \<open>FIXME move\<close>
-  "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
-proof (cases "m < q")
-  case False then show ?thesis by simp
-next
-  case True then show ?thesis by (simp add: upt_conv_Cons)
-qed
-
-
 subsection \<open>Characters and strings\<close>
 
 subsubsection \<open>Characters as finite algebraic type\<close>