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