changeset 72671 | 588c751a5eef |
parent 69085 | 9999d7823b8f |
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy Fri Nov 20 23:53:37 2020 +0100 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy Sat Nov 21 00:29:41 2020 +0100 @@ -5,7 +5,7 @@ section \<open>Theorems about sub arrays\<close> theory Subarray -imports "~~/src/HOL/Imperative_HOL/Array" List_Sublist +imports "../Array" List_Sublist begin definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where