--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Fri Nov 20 23:53:37 2020 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Sat Nov 21 00:29:41 2020 +0100
@@ -6,7 +6,7 @@
theory Imperative_Quicksort
imports
- "~~/src/HOL/Imperative_HOL/Imperative_HOL"
+ "../Imperative_HOL"
Subarray
"HOL-Library.Multiset"
"HOL-Library.Code_Target_Numeral"
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Nov 20 23:53:37 2020 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Sat Nov 21 00:29:41 2020 +0100
@@ -5,7 +5,7 @@
section \<open>An imperative in-place reversal on arrays\<close>
theory Imperative_Reverse
-imports Subarray "~~/src/HOL/Imperative_HOL/Imperative_HOL"
+imports Subarray "../Imperative_HOL"
begin
fun swap :: "'a::heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
--- 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
--- a/src/HOL/Number_Theory/Totient.thy Fri Nov 20 23:53:37 2020 +0100
+++ b/src/HOL/Number_Theory/Totient.thy Sat Nov 21 00:29:41 2020 +0100
@@ -10,7 +10,7 @@
imports
Complex_Main
"HOL-Computational_Algebra.Primes"
- "~~/src/HOL/Number_Theory/Cong"
+ Cong
begin
definition totatives :: "nat \<Rightarrow> nat set" where
--- a/src/HOL/Probability/Random_Permutations.thy Fri Nov 20 23:53:37 2020 +0100
+++ b/src/HOL/Probability/Random_Permutations.thy Sat Nov 21 00:29:41 2020 +0100
@@ -12,7 +12,7 @@
theory Random_Permutations
imports
- "~~/src/HOL/Probability/Probability_Mass_Function"
+ Probability_Mass_Function
"HOL-Library.Multiset_Permutations"
begin