| changeset 41413 | 64cd30d6b0b8 |
| parent 40671 | 5e46057ba8e0 |
| child 42288 | 2074b31650e6 |
--- a/src/HOL/Imperative_HOL/Overview.thy Wed Dec 29 13:51:17 2010 +0100 +++ b/src/HOL/Imperative_HOL/Overview.thy Wed Dec 29 17:34:41 2010 +0100 @@ -4,7 +4,7 @@ (*<*) theory Overview -imports Imperative_HOL LaTeXsugar +imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar" begin (* type constraints with spacing *)