| changeset 20275 | f82435d180ef |
| parent 19233 | 77ca20b0ed77 |
| child 20326 | cbf31171c147 |
--- 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";