# HG changeset patch
# User wenzelm
# Date 1605914981 -3600
# Node ID 588c751a5eef448e1b318624bd9077e4f221ff40
# Parent  4db9411c859cb682d181bce663c7655677a6c294
more standard imports;

diff -r 4db9411c859c -r 588c751a5eef src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- 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"
diff -r 4db9411c859c -r 588c751a5eef src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- 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
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 \<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
diff -r 4db9411c859c -r 588c751a5eef src/HOL/Number_Theory/Totient.thy
--- 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
diff -r 4db9411c859c -r 588c751a5eef src/HOL/Probability/Random_Permutations.thy
--- 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