isabelle: src/HOL/Import/Generate-HOL/GenHOL4Base.thy@3e89a5cab8d7 (annotated)

14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	1	(* Title: HOL/Import/Generate-HOL/GenHOL4Base.thy
41589 bbd861837ebc tuned headers; wenzelm parents: 40607 diff changeset	2	Author: Sebastian Skalberg, TU Muenchen
14620 1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	3	*)
1be590fd2422 Minor cleanup of headers and some speedup of the HOL4 import. skalberg parents: 14516 diff changeset	4
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 15647 diff changeset	5	theory GenHOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	6
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	7	import_segment "hol4";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	8
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	9	setup_dump "../HOL" "HOL4Base";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	10
17566 484ff733f29c new header syntax; wenzelm parents: 17188 diff changeset	11	append_dump {theory HOL4Base imports "../HOL4Compat" "../HOL4Syntax" begin};
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	12
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	13	import_theory "~~/src/HOL/Import/HOL" bool;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	14
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	15	type_maps
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	16	bool > HOL.bool;
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	17
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	18	const_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	19	T > HOL.True
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	20	F > HOL.False
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	21	"!" > HOL.All
38795 848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj haftmann parents: 37678 diff changeset	22	"/\\" > HOL.conj
848be46708dc formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj haftmann parents: 37678 diff changeset	23	"\\/" > HOL.disj
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	24	"?" > HOL.Ex
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	25	"?!" > HOL.Ex1
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	26	"~" > HOL.Not
17188 a26a4fc323ed Updated import. obua parents: 16417 diff changeset	27	COND > HOL.If
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	28	bool_case > Product_Type.bool.bool_case
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	29	ONE_ONE > HOL4Setup.ONE_ONE
17628 f4e2587bc7a5 HOL4-Import: map ONTO to Fun.surj obua parents: 17566 diff changeset	30	ONTO > Fun.surj
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	31	TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	32	LET > HOL4Compat.LET;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	33
44377 d3e609c87c4c reverted some odd changes to HOL/Import (cf. 74c08021ab2e); wenzelm parents: 44367 diff changeset	34	ignore_thms
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	35	BOUNDED_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	36	BOUNDED_THM
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	37	UNBOUNDED_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	38	UNBOUNDED_THM;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	39
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	40	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	41
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	42	import_theory "~~/src/HOL/Import/HOL" combin;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	43
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	44	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	45	o > Fun.comp;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	46
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	47	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	48
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	49	import_theory "~~/src/HOL/Import/HOL" sum;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	50
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	51	type_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	52	sum > Sum_Type.sum;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	53
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	54	const_maps
15647 b1f486a9c56b Updated import configuration. skalberg parents: 14620 diff changeset	55	INL > Sum_Type.Inl
b1f486a9c56b Updated import configuration. skalberg parents: 14620 diff changeset	56	INR > Sum_Type.Inr
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	57	ISL > HOL4Compat.ISL
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	58	ISR > HOL4Compat.ISR
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	59	OUTL > HOL4Compat.OUTL
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	60	OUTR > HOL4Compat.OUTR
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	61	sum_case > Sum_Type.sum.sum_case;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	62
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	63	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	64	sum_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	65	sum_ISO_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	66	IS_SUM_REP
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	67	INL_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	68	INR_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	69	sum_Axiom;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	70
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	71	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	72
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	73	import_theory "~~/src/HOL/Import/HOL" one;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	74
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	75	type_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	76	one > Product_Type.unit;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	77
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	78	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	79	one > Product_Type.Unity;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	80
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	81	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	82	one_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	83	one_axiom
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	84	one_Axiom
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	85	one_DEF;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	86
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	87	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	88
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	89	import_theory "~~/src/HOL/Import/HOL" option;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	90
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	91	type_maps
30235 58d147683393 Made Option a separate theory and renamed option_map to Option.map nipkow parents: 24996 diff changeset	92	option > Option.option;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	93
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	94	const_maps
30235 58d147683393 Made Option a separate theory and renamed option_map to Option.map nipkow parents: 24996 diff changeset	95	NONE > Option.option.None
58d147683393 Made Option a separate theory and renamed option_map to Option.map nipkow parents: 24996 diff changeset	96	SOME > Option.option.Some
58d147683393 Made Option a separate theory and renamed option_map to Option.map nipkow parents: 24996 diff changeset	97	option_case > Option.option.option_case
58d147683393 Made Option a separate theory and renamed option_map to Option.map nipkow parents: 24996 diff changeset	98	OPTION_MAP > Option.map
58d147683393 Made Option a separate theory and renamed option_map to Option.map nipkow parents: 24996 diff changeset	99	THE > Option.the
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	100	IS_SOME > HOL4Compat.IS_SOME
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	101	IS_NONE > HOL4Compat.IS_NONE
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	102	OPTION_JOIN > HOL4Compat.OPTION_JOIN;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	103
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	104	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	105	option_axiom
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	106	option_Axiom
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	107	option_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	108	option_REP_ABS_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	109	SOME_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	110	NONE_DEF;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	111
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	112	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	113
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	114	import_theory "~~/src/HOL/Import/HOL" marker;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	115	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	116
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	117	import_theory "~~/src/HOL/Import/HOL" relation;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	118
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	119	const_renames
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	120	reflexive > pred_reflexive;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	121
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	122	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	123
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	124	import_theory "~~/src/HOL/Import/HOL" pair;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	125
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	126	type_maps
37678 0040bafffdef "prod" and "sum" replace "" and "+" respectively haftmann* parents: 37391 diff changeset	127	prod > Product_Type.prod;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	128
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	129	const_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	130	"," > Product_Type.Pair
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	131	FST > Product_Type.fst
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	132	SND > Product_Type.snd
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	133	CURRY > Product_Type.curry
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	134	UNCURRY > Product_Type.prod.prod_case
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	135	"##" > Product_Type.map_pair
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	136	pair_case > Product_Type.prod.prod_case;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	137
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	138	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	139	prod_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	140	MK_PAIR_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	141	IS_PAIR_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	142	ABS_REP_prod
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	143	COMMA_DEF;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	144
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	145	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	146
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	147	import_theory "~~/src/HOL/Import/HOL" num;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	148
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	149	type_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	150	num > Nat.nat;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	151
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	152	const_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	153	SUC > Nat.Suc
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	154	0 > Groups.zero_class.zero :: nat;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	155
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	156	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	157	num_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	158	num_ISO_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	159	IS_NUM_REP
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	160	ZERO_REP_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	161	SUC_REP_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	162	ZERO_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	163	SUC_DEF;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	164
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	165	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	166
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	167	import_theory "~~/src/HOL/Import/HOL" prim_rec;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	168
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	169	const_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	170	"<" > Orderings.ord_class.less :: "nat \<Rightarrow> nat \<Rightarrow> bool";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	171
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	172	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	173
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	174	import_theory "~~/src/HOL/Import/HOL" arithmetic;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	175
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	176	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	177	ALT_ZERO > HOL4Compat.ALT_ZERO
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	178	NUMERAL_BIT1 > HOL4Compat.NUMERAL_BIT1
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	179	NUMERAL_BIT2 > HOL4Compat.NUMERAL_BIT2
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	180	NUMERAL > HOL4Compat.NUMERAL
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	181	num_case > Nat.nat.nat_case
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	182	">" > HOL4Compat.nat_gt
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	183	">=" > HOL4Compat.nat_ge
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	184	FUNPOW > HOL4Compat.FUNPOW
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	185	"<=" > Orderings.ord_class.less_eq :: "nat \<Rightarrow> nat \<Rightarrow> bool"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	186	"+" > Groups.plus_class.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	187	"*" > Groups.times_class.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	188	"-" > Groups.minus_class.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	189	MIN > Orderings.ord_class.min :: "nat \<Rightarrow> nat \<Rightarrow> nat"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	190	MAX > Orderings.ord_class.max :: "nat \<Rightarrow> nat \<Rightarrow> nat"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	191	DIV > Divides.div_class.div :: "nat \<Rightarrow> nat \<Rightarrow> nat"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	192	MOD > Divides.div_class.mod :: "nat \<Rightarrow> nat \<Rightarrow> nat"
a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	193	EXP > Power.power_class.power :: "nat \<Rightarrow> nat \<Rightarrow> nat";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	194
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	195	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	196
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	197	import_theory "~~/src/HOL/Import/HOL" hrat;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	198	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	199
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	200	import_theory "~~/src/HOL/Import/HOL" hreal;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	201	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	202
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	203	import_theory "~~/src/HOL/Import/HOL" numeral;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	204	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	205
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	206	import_theory "~~/src/HOL/Import/HOL" ind_type;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	207	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	208
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	209	import_theory "~~/src/HOL/Import/HOL" divides;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	210
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	211	const_maps
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	212	divides > Rings.dvd_class.dvd :: "nat \<Rightarrow> nat \<Rightarrow> bool";
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	213
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	214	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	215
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	216	import_theory "~~/src/HOL/Import/HOL" prime;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	217	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	218
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	219	import_theory "~~/src/HOL/Import/HOL" list;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	220
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	221	type_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	222	list > List.list;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	223
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	224	const_maps
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	225	CONS > List.list.Cons
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	226	NIL > List.list.Nil
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	227	list_case > List.list.list_case
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	228	NULL > List.null
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	229	HD > List.hd
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	230	TL > List.tl
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	231	MAP > List.map
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	232	MEM > HOL4Compat.list_mem
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	233	FILTER > List.filter
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	234	FOLDL > List.foldl
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	235	EVERY > List.list_all
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	236	REVERSE > List.rev
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	237	LAST > List.last
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	238	FRONT > List.butlast
23029 79ee75dc1e59 constant op @ now named append haftmann parents: 22997 diff changeset	239	APPEND > List.append
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	240	FLAT > List.concat
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	241	LENGTH > Nat.size_class.size
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	242	REPLICATE > List.replicate
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	243	list_size > HOL4Compat.list_size
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	244	SUM > HOL4Compat.sum
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	245	FOLDR > HOL4Compat.FOLDR
44740 a2940bc24bad HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 44377 diff changeset	246	EXISTS > List.list_ex
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	247	MAP2 > HOL4Compat.map2
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	248	ZIP > HOL4Compat.ZIP
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	249	UNZIP > HOL4Compat.unzip;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	250
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	251	ignore_thms
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	252	list_TY_DEF
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	253	list_repfns
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	254	list0_def
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	255	list1_def
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	256	NIL
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	257	CONS_def;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	258
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	259	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	260
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	261	import_theory "~~/src/HOL/Import/HOL" pred_set;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	262	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	263
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	264	import_theory "~~/src/HOL/Import/HOL" operator;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	265	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	266
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	267	import_theory "~~/src/HOL/Import/HOL" rich_list;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	268	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	269
46780 ab4f3f765f91 explicit locations for import_theory and setup_theory, for better user interface conformance haftmann parents: 44740 diff changeset	270	import_theory "~~/src/HOL/Import/HOL" state_transformer;
14516 a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	271	end_import;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	272
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	273	append_dump "end";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	274
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	275	flush_dump;
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	276
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	277	import_segment "";
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	278
a183dec876ab Added HOL proof importer. skalberg parents: diff changeset	279	end

author	haftmann
	Sat, 03 Mar 2012 21:01:23 +0100
changeset 46783	3e89a5cab8d7
parent 46780	ab4f3f765f91
permissions	-rw-r--r--