diff -r 450cefec7c11 -r cc19f7ca2ed6 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Kildall's Algorithm \label{sec:Kildall}\<close>
 
 theory Kildall
-imports SemilatAlg "~~/src/HOL/Library/While_Combinator"
+imports SemilatAlg "HOL-Library.While_Combinator"
 begin
 
 primrec propa :: "'s binop \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's list \<Rightarrow> nat set \<Rightarrow> 's list * nat set" where