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