changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 69597 | ff784d5a5bfb |
--- a/src/HOL/Imperative_HOL/Overview.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Imperative_HOL/Overview.thy Fri Aug 18 20:47:47 2017 +0200 @@ -4,7 +4,7 @@ (*<*) theory Overview -imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar" +imports Imperative_HOL "HOL-Library.LaTeXsugar" begin (* type constraints with spacing *)