changeset 41589 | bbd861837ebc |
parent 38864 | 4abe644fcea5 |
child 43785 | 2bd54d4b5f3d |
41588:9546828c0eb3 | 41589:bbd861837ebc |
---|---|
1 (* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy |
1 (* Title: HOL/Import/Generate-HOLLight/GenHOLLight.thy |
2 ID: $Id$ |
2 Author: Steven Obua, TU Muenchen |
3 Author: Steven Obua (TU Muenchen) |
|
4 *) |
3 *) |
5 |
4 |
6 theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin; |
5 theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin; |
7 |
6 |
8 (*;skip_import_dir "/home/obua/tmp/cache" |
7 (*;skip_import_dir "/home/obua/tmp/cache" |