state: body context;
added theory_context, proof_to_theory_context;
added is_proof, level;
turned excursion_result into present_excursion;
(* 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