src/HOL/Import/HOL4Syntax.thy
author wenzelm
Sun Jan 16 15:53:03 2011 +0100 (2011-01-16)
changeset 41589 bbd861837ebc
parent 16417 9bc16273c2d4
child 46783 3e89a5cab8d7
permissions -rw-r--r--
tuned headers;
skalberg@14620
     1
(*  Title:      HOL/Import/HOL4Syntax.thy
wenzelm@41589
     2
    Author:     Sebastian Skalberg, TU Muenchen
skalberg@14620
     3
*)
skalberg@14620
     4
wenzelm@41589
     5
theory HOL4Syntax
wenzelm@41589
     6
imports HOL4Setup
wenzelm@41589
     7
uses "import_syntax.ML"
wenzelm@41589
     8
begin
skalberg@14516
     9
skalberg@14516
    10
ML {* HOL4ImportSyntax.setup() *}
skalberg@14516
    11
skalberg@14516
    12
end