changeset 46780 | ab4f3f765f91 |
parent 44860 | 56101fa00193 |
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sat Mar 03 14:04:49 2012 +0100 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Sat Mar 03 21:00:04 2012 +0100 @@ -11,7 +11,7 @@ ;append_dump {*theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin *} -;import_theory hollight +import_theory "~~/src/HOL/Import/HOLLight" hollight ;ignore_thms (* Unit type *)