src/HOL/Import/Import_Setup.thy
author wenzelm
Mon, 30 Jun 2025 20:44:40 +0200
changeset 82800 476627cac12e
parent 81933 cb05f8d3fd05
permissions -rw-r--r--
NEWS;

(*  Title:      HOL/Import/Import_Setup.thy
    Author:     Cezary Kaliszyk, University of Innsbruck
    Author:     Alexander Krauss, QAware GmbH
    Author:     Makarius
*)

section \<open>Importer machinery\<close>

theory Import_Setup
imports Main
keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
begin

ML_file \<open>import_data.ML\<close>

text \<open>
  Initial type and constant maps, for types and constants that are not
  defined, which means their definitions do not appear in the proof dump.
\<close>
import_type_map bool : bool
import_type_map "fun" : "fun"
import_type_map ind : ind
import_const_map "=" : HOL.eq
import_const_map "@" : Eps

ML_file \<open>import_rule.ML\<close>

end