| changeset 66453 | cc19f7ca2ed6 |
| parent 66404 | 7eb451adbda6 |
| child 67226 | ec32cdaab97b |
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Fri Aug 18 20:47:47 2017 +0200 @@ -6,9 +6,9 @@ theory Generate_Efficient_Datastructures imports Candidates - "~~/src/HOL/Library/DAList_Multiset" - "~~/src/HOL/Library/RBT_Mapping" - "~~/src/HOL/Library/RBT_Set" + "HOL-Library.DAList_Multiset" + "HOL-Library.RBT_Mapping" + "HOL-Library.RBT_Set" begin text \<open>