equal
deleted
inserted
replaced
3 section \<open>Character and string types\<close> |
3 section \<open>Character and string types\<close> |
4 |
4 |
5 theory String |
5 theory String |
6 imports Enum |
6 imports Enum |
7 begin |
7 begin |
8 |
|
9 lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close> -- \<open>FIXME move\<close> |
|
10 "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]" |
|
11 proof (cases "m < q") |
|
12 case False then show ?thesis by simp |
|
13 next |
|
14 case True then show ?thesis by (simp add: upt_conv_Cons) |
|
15 qed |
|
16 |
|
17 |
8 |
18 subsection \<open>Characters and strings\<close> |
9 subsection \<open>Characters and strings\<close> |
19 |
10 |
20 subsubsection \<open>Characters as finite algebraic type\<close> |
11 subsubsection \<open>Characters as finite algebraic type\<close> |
21 |
12 |