src/HOL/Import/import_syntax.ML
changeset 46807 04f2d3c510d0
parent 46806 cc47e252b92c
child 46808 a4ae06650a0a
equal deleted inserted replaced
46806:cc47e252b92c 46807:04f2d3c510d0
     1 (*  Title:      HOL/Import/import_syntax.ML
       
     2     Author:     Sebastian Skalberg (TU Muenchen)
       
     3 *)
       
     4 
       
     5 signature IMPORTER_IMPORT_SYNTAX =
       
     6 sig
       
     7 end
       
     8 
       
     9 structure Importer_Import_Syntax : IMPORTER_IMPORT_SYNTAX =
       
    10 struct
       
    11 
       
    12 end