Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/Import_Setup.thy
author haftmann
Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734 89347c0cc6a3
parent 81933 cb05f8d3fd05
permissions -rw-r--r--
treat map_filter similar to list_all, list_ex, list_ex1

(*  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
isabelle