src/Doc/Sugar/Sugar.thy
changeset 66453 cc19f7ca2ed6
parent 64267 b9a1486e79be
child 66527 7ca69030a2af
--- a/src/Doc/Sugar/Sugar.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/Doc/Sugar/Sugar.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -1,8 +1,8 @@
 (*<*)
 theory Sugar
 imports
-  "~~/src/HOL/Library/LaTeXsugar"
-  "~~/src/HOL/Library/OptionalSugar"
+  "HOL-Library.LaTeXsugar"
+  "HOL-Library.OptionalSugar"
 begin
 no_translations
   ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"