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

author	haftmann
	Sat, 03 Mar 2012 23:43:21 +0100
changeset 46796	81e5ec0a3cd0
parent 46787	3d3d8f8929a7
child 46879	a8b1236e0837
permissions	-rw-r--r--