src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
changeset 66453 cc19f7ca2ed6
parent 63167 0909deb8059b
child 74592 3c587b7c3d5c
--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -6,9 +6,9 @@
 theory Generate_Target_Nat
 imports
   Candidates
-  "~~/src/HOL/Library/AList_Mapping"
-  "~~/src/HOL/Library/Finite_Lattice"
-  "~~/src/HOL/Library/Code_Target_Numeral"
+  "HOL-Library.AList_Mapping"
+  "HOL-Library.Finite_Lattice"
+  "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>