author | obua |
Tue, 01 Aug 2006 13:51:16 +0200 | |
changeset 20275 | f82435d180ef |
parent 20274 | 2d60a6ed67f1 |
child 20276 | d94dc40673b1 |
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Tue Aug 01 13:44:05 2006 +0200 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Tue Aug 01 13:51:16 2006 +0200 @@ -5,9 +5,9 @@ theory GenHOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin; -;skip_import_dir "/home/obua/tmp/cache" +(*;skip_import_dir "/home/obua/tmp/cache" -;skip_import on +;skip_import on*) ;import_segment "hollight";