src/HOL/ex/Computations.thy

--- a/src/HOL/ex/Computations.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/ex/Computations.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Simple example for computations generated by the code generator\<close>
 
 theory Computations
-  imports "../Nat" "../Fun_Def" "../Num" "../Code_Numeral"
+  imports HOL.Nat HOL.Fun_Def HOL.Num HOL.Code_Numeral
 begin
 
 fun even :: "nat \<Rightarrow> bool"