src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
changeset 41589 bbd861837ebc
parent 38864 4abe644fcea5
child 43785 2bd54d4b5f3d
equal deleted inserted replaced
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"