(* Title: HOL/Import/HOL4Syntax.thy Author: Sebastian Skalberg, TU Muenchen *) theory HOL4Syntax imports HOL4Setup uses "import_syntax.ML" begin ML {* HOL4ImportSyntax.setup() *} end