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