diff -r 4db9411c859c -r 588c751a5eef src/HOL/Imperative_HOL/ex/Subarray.thy --- 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 \Theorems about sub arrays\ theory Subarray -imports "~~/src/HOL/Imperative_HOL/Array" List_Sublist +imports "../Array" List_Sublist begin definition subarray :: "nat \ nat \ ('a::heap) array \ heap \ 'a list" where