| changeset 63167 | 0909deb8059b |
| parent 62390 | 842917225d56 |
| child 65956 | 639eb3617a86 |
| 63166:143f58bb34f9 | 63167:0909deb8059b |
|---|---|
1 (* Title: HOL/Imperative_HOL/ex/Subarray.thy |
1 (* Title: HOL/Imperative_HOL/ex/Subarray.thy |
2 Author: Lukas Bulwahn, TU Muenchen |
2 Author: Lukas Bulwahn, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 section {* Theorems about sub arrays *} |
5 section \<open>Theorems about sub arrays\<close> |
6 |
6 |
7 theory Subarray |
7 theory Subarray |
8 imports "~~/src/HOL/Imperative_HOL/Array" List_Sublist |
8 imports "~~/src/HOL/Imperative_HOL/Array" List_Sublist |
9 begin |
9 begin |
10 |
10 |