| changeset 17915 | e38947f9ba5e |
| parent 17652 | b1ef33ebfa17 |
| child 19093 | 6d584f9d2021 |
--- a/src/HOL/Import/HOLLight/HOLLight.thy Wed Oct 19 21:52:07 2005 +0200 +++ b/src/HOL/Import/HOLLight/HOLLight.thy Wed Oct 19 21:52:27 2005 +0200 @@ -1,6 +1,6 @@ (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) -theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax": +theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin ;setup_theory hollight