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"