--- 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
--- 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>