src/HOL/Imperative_HOL/ex/Subarray.thy
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