isabelle: src/HOL/Import/Import_Setup.thy@cb05f8d3fd05 (annotated)

47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	1	(* Title: HOL/Import/Import_Setup.thy
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	2	Author: Cezary Kaliszyk, University of Innsbruck
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	3	Author: Alexander Krauss, QAware GmbH
81933 cb05f8d3fd05 more comments; wenzelm parents: 81904 diff changeset	4	Author: Makarius
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	5	*)
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	6
81829 ca1ad6660b4a tuned: prefer inlined thms; wenzelm parents: 81828 diff changeset	7	section \<open>Importer machinery\<close>
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	8
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	9	theory Import_Setup
65552 f533820e7248 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications; wenzelm parents: 63167 diff changeset	10	imports Main
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47258 diff changeset	11	keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	12	begin
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	13
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 65552 diff changeset	14	ML_file \<open>import_data.ML\<close>
81904 aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	15
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	16	text \<open>
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	17	Initial type and constant maps, for types and constants that are not
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	18	defined, which means their definitions do not appear in the proof dump.
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	19	\<close>
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	20	import_type_map bool : bool
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	21	import_type_map "fun" : "fun"
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	22	import_type_map ind : ind
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	23	import_const_map "=" : HOL.eq
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	24	import_const_map "@" : Eps
aa28d82d6b66 tuned; wenzelm parents: 81829 diff changeset	25
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 65552 diff changeset	26	ML_file \<open>import_rule.ML\<close>
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	27
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	28	end

author	wenzelm
	Mon, 20 Jan 2025 23:00:17 +0100
changeset 81933	cb05f8d3fd05
parent 81904	aa28d82d6b66
permissions	-rw-r--r--