isabelle: src/HOL/Import/Import_Setup.thy@ca1ad6660b4a (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
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	4	*)
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	5
81829 ca1ad6660b4a tuned: prefer inlined thms; wenzelm parents: 81828 diff changeset	6	section \<open>Importer machinery\<close>
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	7
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	8	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	9	imports Main
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47258 diff changeset	10	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	11	begin
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	12
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 65552 diff changeset	13	ML_file \<open>import_data.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 65552 diff changeset	14	ML_file \<open>import_rule.ML\<close>
47258 880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	15
880e587eee9f Modernized HOL-Import for HOL Light Cezary Kaliszyk <cezarykaliszyk@gmail.com> parents: diff changeset	16	end

author	wenzelm
	Thu, 16 Jan 2025 12:41:55 +0100
changeset 81829	ca1ad6660b4a
parent 81828	b93e6b458433
child 81904	aa28d82d6b66
permissions	-rw-r--r--