| changeset 47108 | 2a1953f0d20d |
| parent 44890 | 22f665a2e91c |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Sat Mar 24 16:27:04 2012 +0100 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Sun Mar 25 20:15:39 2012 +0200 @@ -5,7 +5,7 @@ header {* Theorems about sub arrays *} theory Subarray -imports Array Sublist +imports "~~/src/HOL/Imperative_HOL/Array" Sublist begin definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where