equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* Slices of lists *} |
5 header {* Slices of lists *} |
6 |
6 |
7 theory Sublist |
7 theory Sublist |
8 imports Multiset |
8 imports "~~/src/HOL/Library/Multiset" |
9 begin |
9 begin |
10 |
10 |
11 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" |
11 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" |
12 apply (induct xs arbitrary: i j k) |
12 apply (induct xs arbitrary: i j k) |
13 apply simp |
13 apply simp |