equal
deleted
inserted
replaced
|
1 (* Title: HOL/Imperative_HOL/ex/Subarray.thy |
|
2 Author: Lukas Bulwahn, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Theorems about sub arrays *} |
|
6 |
1 theory Subarray |
7 theory Subarray |
2 imports Array Sublist |
8 imports Array Sublist |
3 begin |
9 begin |
4 |
10 |
5 definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" |
11 definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" |