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