src/HOL/String.thy
changeset 62580 7011429f44f9
parent 62364 9209770bdcdf
child 62597 b3f2b8c906a6
     1.1 --- a/src/HOL/String.thy	Wed Mar 09 21:01:22 2016 +0100
     1.2 +++ b/src/HOL/String.thy	Thu Mar 10 12:33:01 2016 +0100
     1.3 @@ -6,15 +6,6 @@
     1.4  imports Enum
     1.5  begin
     1.6  
     1.7 -lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close> -- \<open>FIXME move\<close>
     1.8 -  "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
     1.9 -proof (cases "m < q")
    1.10 -  case False then show ?thesis by simp
    1.11 -next
    1.12 -  case True then show ?thesis by (simp add: upt_conv_Cons)
    1.13 -qed
    1.14 -
    1.15 -
    1.16  subsection \<open>Characters and strings\<close>
    1.17  
    1.18  subsubsection \<open>Characters as finite algebraic type\<close>