wneuper/isa: src/HOL/Import/HOLLight/hollight.imp@6ca79a354c51 (annotated)

obua@17644	1	import
obua@17644	2
obua@17644	3	import_segment "hollight"
obua@17644	4
kaliszyk@44639	5	def_maps
kaliszyk@44639	6	"vector" > "vector_def"
kaliszyk@44639	7	"treal_of_num" > "treal_of_num_def"
kaliszyk@44639	8	"treal_neg" > "treal_neg_def"
kaliszyk@44639	9	"treal_mul" > "treal_mul_def"
kaliszyk@44639	10	"treal_le" > "treal_le_def"
kaliszyk@44639	11	"treal_inv" > "treal_inv_def"
kaliszyk@44639	12	"treal_eq" > "treal_eq_def"
kaliszyk@44639	13	"treal_add" > "treal_add_def"
kaliszyk@44639	14	"tailadmissible" > "tailadmissible_def"
kaliszyk@44639	15	"support" > "support_def"
kaliszyk@44639	16	"superadmissible" > "superadmissible_def"
kaliszyk@44639	17	"sum" > "sum_def"
kaliszyk@44639	18	"sndcart" > "sndcart_def"
kaliszyk@44639	19	"rem" > "rem_def"
kaliszyk@44639	20	"real_sub" > "real_sub_def"
kaliszyk@44639	21	"real_sgn" > "real_sgn_def"
kaliszyk@44639	22	"real_pow" > "real_pow_def"
kaliszyk@44639	23	"real_of_num" > "real_of_num_def"
kaliszyk@44639	24	"real_neg" > "real_neg_def"
kaliszyk@44639	25	"real_mul" > "real_mul_def"
kaliszyk@44639	26	"real_mod" > "real_mod_def"
kaliszyk@44639	27	"real_min" > "real_min_def"
kaliszyk@44639	28	"real_max" > "real_max_def"
kaliszyk@44639	29	"real_lt" > "real_lt_def"
kaliszyk@44639	30	"real_le" > "real_le_def"
kaliszyk@44639	31	"real_inv" > "real_inv_def"
kaliszyk@44639	32	"real_gt" > "real_gt_def"
kaliszyk@44639	33	"real_ge" > "real_ge_def"
kaliszyk@44639	34	"real_div" > "real_div_def"
kaliszyk@44639	35	"real_add" > "real_add_def"
kaliszyk@44639	36	"real_abs" > "real_abs_def"
kaliszyk@44639	37	"pastecart" > "pastecart_def"
kaliszyk@44639	38	"pairwise" > "pairwise_def"
kaliszyk@44639	39	"num_of_int" > "num_of_int_def"
kaliszyk@44639	40	"num_mod" > "num_mod_def"
kaliszyk@44639	41	"num_gcd" > "num_gcd_def"
kaliszyk@44639	42	"num_divides" > "num_divides_def"
kaliszyk@44639	43	"num_coprime" > "num_coprime_def"
kaliszyk@44639	44	"nsum" > "nsum_def"
kaliszyk@44639	45	"neutral" > "neutral_def"
kaliszyk@44639	46	"nadd_rinv" > "nadd_rinv_def"
kaliszyk@44639	47	"nadd_of_num" > "nadd_of_num_def"
kaliszyk@44639	48	"nadd_mul" > "nadd_mul_def"
kaliszyk@44639	49	"nadd_le" > "nadd_le_def"
kaliszyk@44639	50	"nadd_inv" > "nadd_inv_def"
kaliszyk@44639	51	"nadd_eq" > "nadd_eq_def"
kaliszyk@44639	52	"nadd_add" > "nadd_add_def"
kaliszyk@44639	53	"monoidal" > "monoidal_def"
kaliszyk@44639	54	"minimal" > "minimal_def"
kaliszyk@44639	55	"lambda" > "lambda_def"
kaliszyk@44639	56	"iterate" > "iterate_def"
kaliszyk@44639	57	"is_nadd" > "is_nadd_def"
kaliszyk@44639	58	"integer" > "integer_def"
kaliszyk@44639	59	"int_sub" > "int_sub_def"
kaliszyk@44639	60	"int_sgn" > "int_sgn_def"
kaliszyk@44639	61	"int_pow" > "int_pow_def"
kaliszyk@44639	62	"int_of_num" > "int_of_num_def"
kaliszyk@44639	63	"int_neg" > "int_neg_def"
kaliszyk@44639	64	"int_mul" > "int_mul_def"
kaliszyk@44639	65	"int_mod" > "int_mod_def"
kaliszyk@44639	66	"int_min" > "int_min_def"
kaliszyk@44639	67	"int_max" > "int_max_def"
kaliszyk@44639	68	"int_lt" > "int_lt_def"
kaliszyk@44639	69	"int_le" > "int_le_def"
kaliszyk@44639	70	"int_gt" > "int_gt_def"
kaliszyk@44639	71	"int_ge" > "int_ge_def"
kaliszyk@44639	72	"int_gcd" > "int_gcd_def"
kaliszyk@44639	73	"int_divides" > "int_divides_def"
kaliszyk@44639	74	"int_coprime" > "int_coprime_def"
kaliszyk@44639	75	"int_add" > "int_add_def"
kaliszyk@44639	76	"int_abs" > "int_abs_def"
kaliszyk@44639	77	"hreal_of_num" > "hreal_of_num_def"
kaliszyk@44639	78	"hreal_mul" > "hreal_mul_def"
kaliszyk@44639	79	"hreal_le" > "hreal_le_def"
kaliszyk@44639	80	"hreal_inv" > "hreal_inv_def"
kaliszyk@44639	81	"hreal_add" > "hreal_add_def"
kaliszyk@44639	82	"fstcart" > "fstcart_def"
kaliszyk@44639	83	"eqeq" > "eqeq_def"
kaliszyk@44639	84	"div" > "div_def"
kaliszyk@44639	85	"dist" > "dist_def"
kaliszyk@44639	86	"dimindex" > "dimindex_def"
kaliszyk@44639	87	"admissible" > "admissible_def"
kaliszyk@44639	88	"_UNGUARDED_PATTERN" > "_UNGUARDED_PATTERN_def"
kaliszyk@44639	89	"_SEQPATTERN" > "_SEQPATTERN_def"
kaliszyk@44639	90	"_MATCH" > "_MATCH_def"
kaliszyk@44639	91	"_GUARDED_PATTERN" > "_GUARDED_PATTERN_def"
kaliszyk@44639	92	"_FUNCTION" > "_FUNCTION_def"
kaliszyk@44639	93	"_FALSITY_" > "_FALSITY__def"
kaliszyk@44639	94	"_11937" > "_11937_def"
kaliszyk@44639	95	"ZRECSPACE" > "ZRECSPACE_def"
kaliszyk@44639	96	"ZCONSTR" > "ZCONSTR_def"
kaliszyk@44639	97	"ZBOT" > "ZBOT_def"
kaliszyk@44639	98	"UNCURRY" > "UNCURRY_def"
kaliszyk@44639	99	"SURJ" > "SURJ_def"
kaliszyk@44639	100	"SING" > "SING_def"
kaliszyk@44639	101	"REST" > "REST_def"
kaliszyk@44639	102	"PASSOC" > "PASSOC_def"
kaliszyk@44639	103	"PAIRWISE" > "PAIRWISE_def"
kaliszyk@44639	104	"NUM_REP" > "NUM_REP_def"
kaliszyk@44639	105	"NUMSUM" > "NUMSUM_def"
kaliszyk@44639	106	"NUMSND" > "NUMSND_def"
kaliszyk@44639	107	"NUMRIGHT" > "NUMRIGHT_def"
kaliszyk@44639	108	"NUMPAIR" > "NUMPAIR_def"
kaliszyk@44639	109	"NUMLEFT" > "NUMLEFT_def"
kaliszyk@44639	110	"NUMFST" > "NUMFST_def"
kaliszyk@44639	111	"LET_END" > "LET_END_def"
kaliszyk@44639	112	"ITSET" > "ITSET_def"
kaliszyk@44639	113	"ISO" > "ISO_def"
kaliszyk@44639	114	"INJP" > "INJP_def"
kaliszyk@44639	115	"INJN" > "INJN_def"
kaliszyk@44639	116	"INJF" > "INJF_def"
kaliszyk@44639	117	"INJA" > "INJA_def"
kaliszyk@44639	118	"INJ" > "INJ_def"
kaliszyk@44639	119	"IND_SUC" > "IND_SUC_def"
kaliszyk@44639	120	"IND_0" > "IND_0_def"
kaliszyk@44639	121	"HAS_SIZE" > "HAS_SIZE_def"
kaliszyk@44639	122	"FNIL" > "FNIL_def"
kaliszyk@44639	123	"FINREC" > "FINREC_def"
kaliszyk@44639	124	"FCONS" > "FCONS_def"
kaliszyk@44639	125	"DECIMAL" > "DECIMAL_def"
kaliszyk@44639	126	"CROSS" > "CROSS_def"
kaliszyk@44639	127	"COUNTABLE" > "COUNTABLE_def"
kaliszyk@44639	128	"CONSTR" > "CONSTR_def"
kaliszyk@44639	129	"CASEWISE" > "CASEWISE_def"
kaliszyk@44639	130	"CARD" > "CARD_def"
kaliszyk@44639	131	"BOTTOM" > "BOTTOM_def"
kaliszyk@44639	132	"BIJ" > "BIJ_def"
kaliszyk@44639	133	"ASCII" > "ASCII_def"
kaliszyk@44639	134	">_c" > ">_c_def"
kaliszyk@44639	135	">=_c" > ">=_c_def"
kaliszyk@44639	136	"=_c" > "=_c_def"
kaliszyk@44639	137	"<_c" > "<_c_def"
kaliszyk@44639	138	"<=_c" > "<=_c_def"
kaliszyk@44639	139	"$" > "$_def"
kaliszyk@44639	140
obua@17644	141	type_maps
kaliszyk@44639	142	"sum" > "Sum_Type.sum"
obua@17644	143	"recspace" > "HOLLight.hollight.recspace"
obua@17644	144	"real" > "HOLLight.hollight.real"
haftmann@37678	145	"prod" > "Product_Type.prod"
kaliszyk@44639	146	"option" > "Datatype.option"
haftmann@37362	147	"num" > "Nat.nat"
obua@17644	148	"nadd" > "HOLLight.hollight.nadd"
kaliszyk@44639	149	"list" > "List.list"
obua@17644	150	"int" > "HOLLight.hollight.int"
obua@17644	151	"ind" > "Nat.ind"
obua@17644	152	"hreal" > "HOLLight.hollight.hreal"
obua@17644	153	"fun" > "fun"
obua@17644	154	"finite_sum" > "HOLLight.hollight.finite_sum"
obua@17644	155	"finite_image" > "HOLLight.hollight.finite_image"
kaliszyk@44639	156	"char" > "HOLLight.hollight.char"
obua@17644	157	"cart" > "HOLLight.hollight.cart"
haftmann@38781	158	"bool" > "HOL.bool"
obua@17644	159	"N_3" > "HOLLight.hollight.N_3"
obua@17644	160	"N_2" > "HOLLight.hollight.N_2"
obua@17644	161	"N_1" > "Product_Type.unit"
obua@17644	162
obua@17644	163	const_maps
haftmann@38781	164	"~" > "HOL.Not"
kaliszyk@44639	165	"vector" > "HOLLight.hollight.vector"
obua@17644	166	"treal_of_num" > "HOLLight.hollight.treal_of_num"
obua@17644	167	"treal_neg" > "HOLLight.hollight.treal_neg"
obua@17644	168	"treal_mul" > "HOLLight.hollight.treal_mul"
obua@17644	169	"treal_le" > "HOLLight.hollight.treal_le"
obua@17644	170	"treal_inv" > "HOLLight.hollight.treal_inv"
obua@17644	171	"treal_eq" > "HOLLight.hollight.treal_eq"
obua@17644	172	"treal_add" > "HOLLight.hollight.treal_add"
obua@17644	173	"tailadmissible" > "HOLLight.hollight.tailadmissible"
obua@17644	174	"support" > "HOLLight.hollight.support"
obua@17644	175	"superadmissible" > "HOLLight.hollight.superadmissible"
obua@17644	176	"sum" > "HOLLight.hollight.sum"
obua@17644	177	"sndcart" > "HOLLight.hollight.sndcart"
kaliszyk@44639	178	"set_of_list" > "List.set"
kaliszyk@44639	179	"rem" > "HOLLight.hollight.rem"
obua@17644	180	"real_sub" > "HOLLight.hollight.real_sub"
kaliszyk@44639	181	"real_sgn" > "HOLLight.hollight.real_sgn"
obua@17644	182	"real_pow" > "HOLLight.hollight.real_pow"
obua@17644	183	"real_of_num" > "HOLLight.hollight.real_of_num"
obua@17644	184	"real_neg" > "HOLLight.hollight.real_neg"
obua@17644	185	"real_mul" > "HOLLight.hollight.real_mul"
kaliszyk@44639	186	"real_mod" > "HOLLight.hollight.real_mod"
obua@17644	187	"real_min" > "HOLLight.hollight.real_min"
obua@17644	188	"real_max" > "HOLLight.hollight.real_max"
obua@17644	189	"real_lt" > "HOLLight.hollight.real_lt"
obua@17644	190	"real_le" > "HOLLight.hollight.real_le"
obua@17644	191	"real_inv" > "HOLLight.hollight.real_inv"
obua@17644	192	"real_gt" > "HOLLight.hollight.real_gt"
obua@17644	193	"real_ge" > "HOLLight.hollight.real_ge"
obua@17644	194	"real_div" > "HOLLight.hollight.real_div"
obua@17644	195	"real_add" > "HOLLight.hollight.real_add"
obua@17644	196	"real_abs" > "HOLLight.hollight.real_abs"
obua@17644	197	"pastecart" > "HOLLight.hollight.pastecart"
obua@17644	198	"pairwise" > "HOLLight.hollight.pairwise"
obua@17644	199	"one" > "Product_Type.Unity"
obua@17644	200	"o" > "Fun.comp"
kaliszyk@44639	201	"num_of_int" > "HOLLight.hollight.num_of_int"
kaliszyk@44639	202	"num_mod" > "HOLLight.hollight.num_mod"
kaliszyk@44639	203	"num_gcd" > "HOLLight.hollight.num_gcd"
kaliszyk@44639	204	"num_divides" > "HOLLight.hollight.num_divides"
kaliszyk@44639	205	"num_coprime" > "HOLLight.hollight.num_coprime"
obua@17644	206	"nsum" > "HOLLight.hollight.nsum"
obua@17644	207	"neutral" > "HOLLight.hollight.neutral"
obua@17644	208	"nadd_rinv" > "HOLLight.hollight.nadd_rinv"
obua@17644	209	"nadd_of_num" > "HOLLight.hollight.nadd_of_num"
obua@17644	210	"nadd_mul" > "HOLLight.hollight.nadd_mul"
obua@17644	211	"nadd_le" > "HOLLight.hollight.nadd_le"
obua@17644	212	"nadd_inv" > "HOLLight.hollight.nadd_inv"
obua@17644	213	"nadd_eq" > "HOLLight.hollight.nadd_eq"
obua@17644	214	"nadd_add" > "HOLLight.hollight.nadd_add"
obua@17644	215	"monoidal" > "HOLLight.hollight.monoidal"
obua@17644	216	"mk_pair" > "Product_Type.Pair_Rep"
kaliszyk@44639	217	"mk_num" > "Fun.id"
obua@17644	218	"minimal" > "HOLLight.hollight.minimal"
kaliszyk@44639	219	"list_EX" > "List.list_ex"
kaliszyk@44639	220	"list_ALL" > "List.list_all"
obua@17644	221	"lambda" > "HOLLight.hollight.lambda"
obua@17644	222	"iterate" > "HOLLight.hollight.iterate"
obua@17644	223	"is_nadd" > "HOLLight.hollight.is_nadd"
kaliszyk@44639	224	"integer" > "HOLLight.hollight.integer"
obua@17644	225	"int_sub" > "HOLLight.hollight.int_sub"
kaliszyk@44639	226	"int_sgn" > "HOLLight.hollight.int_sgn"
obua@17644	227	"int_pow" > "HOLLight.hollight.int_pow"
obua@17644	228	"int_of_num" > "HOLLight.hollight.int_of_num"
obua@17644	229	"int_neg" > "HOLLight.hollight.int_neg"
obua@17644	230	"int_mul" > "HOLLight.hollight.int_mul"
kaliszyk@44639	231	"int_mod" > "HOLLight.hollight.int_mod"
obua@17644	232	"int_min" > "HOLLight.hollight.int_min"
obua@17644	233	"int_max" > "HOLLight.hollight.int_max"
obua@17644	234	"int_lt" > "HOLLight.hollight.int_lt"
obua@17644	235	"int_le" > "HOLLight.hollight.int_le"
obua@17644	236	"int_gt" > "HOLLight.hollight.int_gt"
obua@17644	237	"int_ge" > "HOLLight.hollight.int_ge"
kaliszyk@44639	238	"int_gcd" > "HOLLight.hollight.int_gcd"
kaliszyk@44639	239	"int_divides" > "HOLLight.hollight.int_divides"
kaliszyk@44639	240	"int_coprime" > "HOLLight.hollight.int_coprime"
obua@17644	241	"int_add" > "HOLLight.hollight.int_add"
obua@17644	242	"int_abs" > "HOLLight.hollight.int_abs"
obua@17644	243	"hreal_of_num" > "HOLLight.hollight.hreal_of_num"
obua@17644	244	"hreal_mul" > "HOLLight.hollight.hreal_mul"
obua@17644	245	"hreal_le" > "HOLLight.hollight.hreal_le"
obua@17644	246	"hreal_inv" > "HOLLight.hollight.hreal_inv"
obua@17644	247	"hreal_add" > "HOLLight.hollight.hreal_add"
obua@17644	248	"fstcart" > "HOLLight.hollight.fstcart"
obua@17644	249	"eqeq" > "HOLLight.hollight.eqeq"
kaliszyk@44639	250	"div" > "HOLLight.hollight.div"
obua@17644	251	"dist" > "HOLLight.hollight.dist"
obua@17644	252	"dimindex" > "HOLLight.hollight.dimindex"
obua@17644	253	"admissible" > "HOLLight.hollight.admissible"
kaliszyk@44639	254	"_UNGUARDED_PATTERN" > "HOLLight.hollight._UNGUARDED_PATTERN"
kaliszyk@44639	255	"_SEQPATTERN" > "HOLLight.hollight._SEQPATTERN"
kaliszyk@44639	256	"_MATCH" > "HOLLight.hollight._MATCH"
kaliszyk@44639	257	"_GUARDED_PATTERN" > "HOLLight.hollight._GUARDED_PATTERN"
kaliszyk@44639	258	"_FUNCTION" > "HOLLight.hollight._FUNCTION"
obua@17644	259	"_FALSITY_" > "HOLLight.hollight._FALSITY_"
kaliszyk@44639	260	"_11937" > "HOLLight.hollight._11937"
kaliszyk@44639	261	"_0" > "Groups.zero_class.zero" :: "nat"
kaliszyk@44639	262	"\\/" > "HOL.disj"
obua@17644	263	"ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
kaliszyk@44639	264	"ZIP" > "List.zip"
obua@17644	265	"ZCONSTR" > "HOLLight.hollight.ZCONSTR"
obua@17644	266	"ZBOT" > "HOLLight.hollight.ZBOT"
kaliszyk@44639	267	"WF" > "Wellfounded.wfP"
kaliszyk@44639	268	"UNIV" > "Orderings.top_class.top" :: "'a => bool"
kaliszyk@44639	269	"UNIONS" > "Complete_Lattice.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
kaliszyk@44639	270	"UNION" > "Lattices.semilattice_sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
obua@17644	271	"UNCURRY" > "HOLLight.hollight.UNCURRY"
kaliszyk@44639	272	"TL" > "List.tl"
kaliszyk@44639	273	"T" > "HOL.True"
obua@17644	274	"SURJ" > "HOLLight.hollight.SURJ"
haftmann@37362	275	"SUC" > "Nat.Suc"
kaliszyk@44639	276	"SUBSET" > "Orderings.ord_class.less_eq" :: "('a => bool) => ('a => bool) => bool"
kaliszyk@44639	277	"SOME" > "Datatype.Some"
haftmann@37366	278	"SND" > "Product_Type.snd"
obua@17644	279	"SING" > "HOLLight.hollight.SING"
kaliszyk@44639	280	"SETSPEC" > "HOLLightCompat.SETSPEC"
kaliszyk@44639	281	"REVERSE" > "List.rev"
obua@17644	282	"REST" > "HOLLight.hollight.REST"
kaliszyk@44639	283	"REPLICATE" > "List.replicate"
kaliszyk@44639	284	"PSUBSET" > "Orderings.ord_class.less" :: "('a => bool) => ('a => bool) => bool"
obua@17644	285	"PRE" > "HOLLightCompat.Pred"
obua@17644	286	"PASSOC" > "HOLLight.hollight.PASSOC"
obua@17644	287	"PAIRWISE" > "HOLLight.hollight.PAIRWISE"
kaliszyk@44639	288	"OUTR" > "HOLLightCompat.OUTR"
kaliszyk@44639	289	"OUTL" > "HOLLightCompat.OUTL"
obua@17644	290	"ONTO" > "Fun.surj"
kaliszyk@44639	291	"ONE_ONE" > "Fun.inj"
kaliszyk@44639	292	"ODD" > "HOLLightCompat.ODD"
kaliszyk@44639	293	"NUM_REP" > "HOLLight.hollight.NUM_REP"
obua@17644	294	"NUMSUM" > "HOLLight.hollight.NUMSUM"
obua@17644	295	"NUMSND" > "HOLLight.hollight.NUMSND"
obua@17644	296	"NUMRIGHT" > "HOLLight.hollight.NUMRIGHT"
obua@17644	297	"NUMPAIR" > "HOLLight.hollight.NUMPAIR"
obua@17644	298	"NUMLEFT" > "HOLLight.hollight.NUMLEFT"
obua@17644	299	"NUMFST" > "HOLLight.hollight.NUMFST"
kaliszyk@44639	300	"NUMERAL" > "HOLLightCompat.NUMERAL"
kaliszyk@44639	301	"NULL" > "List.null"
kaliszyk@44639	302	"NONE" > "Datatype.None"
kaliszyk@44639	303	"NIL" > "List.list.Nil"
kaliszyk@44639	304	"MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
kaliszyk@44639	305	"MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
kaliszyk@44639	306	"MEM" > "HOLLightList.list_mem"
kaliszyk@44639	307	"MEASURE" > "HOLLightCompat.MEASURE"
kaliszyk@44639	308	"MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
kaliszyk@44639	309	"MAP2" > "HOLLightList.map2"
kaliszyk@44639	310	"MAP" > "List.map"
obua@17644	311	"LET_END" > "HOLLight.hollight.LET_END"
kaliszyk@44639	312	"LET" > "HOLLightCompat.LET"
kaliszyk@44639	313	"LENGTH" > "List.length"
kaliszyk@44639	314	"LAST" > "List.last"
obua@17644	315	"ITSET" > "HOLLight.hollight.ITSET"
kaliszyk@44639	316	"ITLIST2" > "HOLLightList.fold2"
kaliszyk@44639	317	"ITLIST" > "List.foldr"
obua@17644	318	"ISO" > "HOLLight.hollight.ISO"
kaliszyk@44639	319	"INTERS" > "Complete_Lattice.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
kaliszyk@44639	320	"INTER" > "Lattices.semilattice_inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
kaliszyk@44639	321	"INSERT" > "Set.insert"
obua@19093	322	"INR" > "Sum_Type.Inr"
obua@19093	323	"INL" > "Sum_Type.Inl"
obua@17644	324	"INJP" > "HOLLight.hollight.INJP"
obua@17644	325	"INJN" > "HOLLight.hollight.INJN"
obua@17644	326	"INJF" > "HOLLight.hollight.INJF"
obua@17644	327	"INJA" > "HOLLight.hollight.INJA"
obua@17644	328	"INJ" > "HOLLight.hollight.INJ"
kaliszyk@44639	329	"INFINITE" > "HOLLightCompat.INFINITE"
kaliszyk@44639	330	"IND_SUC" > "HOLLight.hollight.IND_SUC"
kaliszyk@44639	331	"IND_0" > "HOLLight.hollight.IND_0"
kaliszyk@44639	332	"IN" > "Set.member"
kaliszyk@44639	333	"IMAGE" > "Set.image"
obua@17644	334	"I" > "Fun.id"
kaliszyk@44639	335	"HD" > "List.hd"
obua@17644	336	"HAS_SIZE" > "HOLLight.hollight.HAS_SIZE"
kaliszyk@44639	337	"GSPEC" > "Set.Collect"
kaliszyk@44639	338	"GEQ" > "HOL.eq"
kaliszyk@44639	339	"GABS" > "Hilbert_Choice.Eps"
haftmann@37366	340	"FST" > "Product_Type.fst"
obua@17644	341	"FNIL" > "HOLLight.hollight.FNIL"
obua@17644	342	"FINREC" > "HOLLight.hollight.FINREC"
kaliszyk@44639	343	"FINITE" > "Finite_Set.finite"
kaliszyk@44639	344	"FILTER" > "List.filter"
obua@17644	345	"FCONS" > "HOLLight.hollight.FCONS"
kaliszyk@44639	346	"FACT" > "Fact.fact_class.fact" :: "nat => nat"
kaliszyk@44639	347	"F" > "HOL.False"
kaliszyk@44639	348	"EXP" > "Power.power_class.power" :: "nat => nat => nat"
kaliszyk@44639	349	"EVEN" > "Parity.even_odd_class.even" :: "nat => bool"
kaliszyk@44639	350	"EMPTY" > "Orderings.bot_class.bot" :: "'a => bool"
kaliszyk@44639	351	"EL" > "HOLLightList.list_el"
kaliszyk@44639	352	"DIV" > "Divides.div_class.div" :: "nat => nat => nat"
kaliszyk@44639	353	"DISJOINT" > "HOLLightCompat.DISJOINT"
kaliszyk@44639	354	"DIFF" > "Groups.minus_class.minus" :: "('a => bool) => ('a => bool) => 'a => bool"
kaliszyk@44639	355	"DELETE" > "HOLLightCompat.DELETE"
obua@17644	356	"DECIMAL" > "HOLLight.hollight.DECIMAL"
kaliszyk@44639	357	"CURRY" > "Product_Type.curry"
kaliszyk@44639	358	"CROSS" > "HOLLight.hollight.CROSS"
obua@17644	359	"COUNTABLE" > "HOLLight.hollight.COUNTABLE"
obua@17644	360	"CONSTR" > "HOLLight.hollight.CONSTR"
kaliszyk@44639	361	"CONS" > "List.list.Cons"
kaliszyk@44639	362	"COND" > "HOL.If"
kaliszyk@44639	363	"CHOICE" > "Hilbert_Choice.Eps"
obua@17644	364	"CASEWISE" > "HOLLight.hollight.CASEWISE"
obua@17644	365	"CARD" > "HOLLight.hollight.CARD"
kaliszyk@44639	366	"BUTLAST" > "List.butlast"
obua@17644	367	"BOTTOM" > "HOLLight.hollight.BOTTOM"
kaliszyk@44639	368	"BIT1" > "HOLLightCompat.NUMERAL_BIT1"
obua@17644	369	"BIT0" > "HOLLightCompat.NUMERAL_BIT0"
obua@17644	370	"BIJ" > "HOLLight.hollight.BIJ"
kaliszyk@44639	371	"ASCII" > "HOLLight.hollight.ASCII"
kaliszyk@44639	372	"APPEND" > "List.append"
kaliszyk@44639	373	"ALL2" > "List.list_all2"
obua@17644	374	"@" > "Hilbert_Choice.Eps"
haftmann@38781	375	"?!" > "HOL.Ex1"
haftmann@38781	376	"?" > "HOL.Ex"
kaliszyk@44639	377	">_c" > "HOLLight.hollight.>_c"
kaliszyk@44639	378	">=_c" > "HOLLight.hollight.>=_c"
kaliszyk@44639	379	">=" > "Orderings.ord_class.greater_eq" :: "nat => nat => bool"
kaliszyk@44639	380	">" > "Orderings.ord_class.greater" :: "nat => nat => bool"
kaliszyk@44639	381	"=_c" > "HOLLight.hollight.=_c"
kaliszyk@44639	382	"==>" > "HOL.implies"
kaliszyk@44639	383	"=" > "HOL.eq"
kaliszyk@44639	384	"<_c" > "HOLLight.hollight.<_c"
kaliszyk@44639	385	"<=_c" > "HOLLight.hollight.<=_c"
kaliszyk@44639	386	"<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
kaliszyk@44639	387	"<" > "Orderings.ord_class.less" :: "nat => nat => bool"
kaliszyk@44639	388	"/\\" > "HOL.conj"
kaliszyk@44639	389	".." > "HOLLightCompat.dotdot"
kaliszyk@44639	390	"-" > "Groups.minus_class.minus" :: "nat => nat => nat"
haftmann@37366	391	"," > "Product_Type.Pair"
kaliszyk@44639	392	"+" > "Groups.plus_class.plus" :: "nat => nat => nat"
kaliszyk@44639	393	"*" > "Groups.times_class.times" :: "nat => nat => nat"
obua@17644	394	"$" > "HOLLight.hollight.$"
haftmann@38781	395	"!" > "HOL.All"
obua@17644	396
obua@17644	397	const_renames
kaliszyk@44639	398	"EX" > "list_EX"
kaliszyk@44639	399	"ALL" > "list_ALL"
obua@17644	400	"==" > "eqeq"
obua@17644	401
obua@17644	402	thm_maps
kaliszyk@44639	403	"vector_def" > "HOLLight.hollight.vector_def"
obua@17644	404	"treal_of_num_def" > "HOLLight.hollight.treal_of_num_def"
obua@17644	405	"treal_neg_def" > "HOLLight.hollight.treal_neg_def"
obua@17644	406	"treal_mul_def" > "HOLLight.hollight.treal_mul_def"
obua@17644	407	"treal_le_def" > "HOLLight.hollight.treal_le_def"
obua@17644	408	"treal_inv_def" > "HOLLight.hollight.treal_inv_def"
obua@17644	409	"treal_eq_def" > "HOLLight.hollight.treal_eq_def"
obua@17644	410	"treal_add_def" > "HOLLight.hollight.treal_add_def"
obua@17644	411	"th_cond" > "HOLLight.hollight.th_cond"
kaliszyk@44639	412	"th" > "HOL.eta_contract_eq"
obua@17644	413	"tailadmissible_def" > "HOLLight.hollight.tailadmissible_def"
obua@17644	414	"support_def" > "HOLLight.hollight.support_def"
obua@17644	415	"superadmissible_def" > "HOLLight.hollight.superadmissible_def"
obua@17644	416	"sum_def" > "HOLLight.hollight.sum_def"
kaliszyk@44639	417	"string_INFINITE" > "List.infinite_UNIV_listI"
obua@17644	418	"sth" > "HOLLight.hollight.sth"
obua@17644	419	"sndcart_def" > "HOLLight.hollight.sndcart_def"
obua@17644	420	"right_th" > "HOLLight.hollight.right_th"
kaliszyk@44639	421	"rem_def" > "HOLLight.hollight.rem_def"
obua@17644	422	"real_sub_def" > "HOLLight.hollight.real_sub_def"
kaliszyk@44639	423	"real_sgn_def" > "HOLLight.hollight.real_sgn_def"
obua@17644	424	"real_pow_def" > "HOLLight.hollight.real_pow_def"
obua@17644	425	"real_of_num_def" > "HOLLight.hollight.real_of_num_def"
obua@17644	426	"real_neg_def" > "HOLLight.hollight.real_neg_def"
obua@17644	427	"real_mul_def" > "HOLLight.hollight.real_mul_def"
kaliszyk@44639	428	"real_mod_def" > "HOLLight.hollight.real_mod_def"
obua@17644	429	"real_min_def" > "HOLLight.hollight.real_min_def"
obua@17644	430	"real_max_def" > "HOLLight.hollight.real_max_def"
obua@17644	431	"real_lt_def" > "HOLLight.hollight.real_lt_def"
obua@17644	432	"real_le_def" > "HOLLight.hollight.real_le_def"
obua@17644	433	"real_inv_def" > "HOLLight.hollight.real_inv_def"
obua@17644	434	"real_gt_def" > "HOLLight.hollight.real_gt_def"
obua@17644	435	"real_ge_def" > "HOLLight.hollight.real_ge_def"
obua@17644	436	"real_div_def" > "HOLLight.hollight.real_div_def"
obua@17644	437	"real_add_def" > "HOLLight.hollight.real_add_def"
obua@17644	438	"real_abs_def" > "HOLLight.hollight.real_abs_def"
kaliszyk@44639	439	"real_INFINITE" > "HOLLight.hollight.real_INFINITE"
obua@17644	440	"pastecart_def" > "HOLLight.hollight.pastecart_def"
obua@17644	441	"pairwise_def" > "HOLLight.hollight.pairwise_def"
obua@17644	442	"pair_RECURSION" > "HOLLight.hollight.pair_RECURSION"
kaliszyk@44639	443	"pair_INDUCT" > "Product_Type.prod.induct"
obua@17644	444	"one_axiom" > "HOLLight.hollight.one_axiom"
obua@17644	445	"one_RECURSION" > "HOLLight.hollight.one_RECURSION"
kaliszyk@44639	446	"one_INDUCT" > "Product_Type.unit.induct"
obua@17644	447	"one_Axiom" > "HOLLight.hollight.one_Axiom"
kaliszyk@44639	448	"one" > "HOLLightCompat.one"
kaliszyk@44639	449	"o_THM" > "Fun.comp_def"
obua@17644	450	"o_ASSOC" > "HOLLight.hollight.o_ASSOC"
kaliszyk@44639	451	"num_of_int_def" > "HOLLight.hollight.num_of_int_def"
kaliszyk@44639	452	"num_mod_def" > "HOLLight.hollight.num_mod_def"
kaliszyk@44639	453	"num_gcd_def" > "HOLLight.hollight.num_gcd_def"
kaliszyk@44639	454	"num_divides_def" > "HOLLight.hollight.num_divides_def"
kaliszyk@44639	455	"num_coprime_def" > "HOLLight.hollight.num_coprime_def"
kaliszyk@44639	456	"num_congruent" > "HOLLight.hollight.num_congruent"
obua@17644	457	"num_WOP" > "HOLLight.hollight.num_WOP"
kaliszyk@44639	458	"num_WF" > "Nat.nat_less_induct"
obua@17644	459	"num_RECURSION_STD" > "HOLLight.hollight.num_RECURSION_STD"
obua@17644	460	"num_MAX" > "HOLLight.hollight.num_MAX"
kaliszyk@44639	461	"num_INFINITE" > "Finite_Set.infinite_UNIV_char_0"
kaliszyk@44639	462	"num_INDUCTION" > "Fact.fact_nat.induct"
obua@17644	463	"num_FINITE_AVOID" > "HOLLight.hollight.num_FINITE_AVOID"
obua@17644	464	"num_FINITE" > "HOLLight.hollight.num_FINITE"
obua@17644	465	"num_CASES" > "Nat.nat.nchotomy"
kaliszyk@44639	466	"num_Axiom" > "HOLLightCompat.num_Axiom"
obua@17644	467	"nsum_def" > "HOLLight.hollight.nsum_def"
obua@17644	468	"neutral_def" > "HOLLight.hollight.neutral_def"
obua@17644	469	"nadd_rinv_def" > "HOLLight.hollight.nadd_rinv_def"
obua@17644	470	"nadd_of_num_def" > "HOLLight.hollight.nadd_of_num_def"
obua@17644	471	"nadd_mul_def" > "HOLLight.hollight.nadd_mul_def"
obua@17644	472	"nadd_le_def" > "HOLLight.hollight.nadd_le_def"
obua@17644	473	"nadd_inv_def" > "HOLLight.hollight.nadd_inv_def"
obua@17644	474	"nadd_eq_def" > "HOLLight.hollight.nadd_eq_def"
obua@17644	475	"nadd_add_def" > "HOLLight.hollight.nadd_add_def"
obua@17644	476	"monoidal_def" > "HOLLight.hollight.monoidal_def"
obua@17644	477	"minimal_def" > "HOLLight.hollight.minimal_def"
kaliszyk@44639	478	"list_INDUCT" > "List.list.induct"
kaliszyk@44639	479	"list_CASES" > "List.list.nchotomy"
obua@17644	480	"lambda_def" > "HOLLight.hollight.lambda_def"
obua@17644	481	"iterate_def" > "HOLLight.hollight.iterate_def"
obua@17644	482	"is_nadd_def" > "HOLLight.hollight.is_nadd_def"
obua@17644	483	"is_nadd_0" > "HOLLight.hollight.is_nadd_0"
kaliszyk@44639	484	"is_int" > "HOLLight.hollight.is_int"
kaliszyk@44639	485	"integer_def" > "HOLLight.hollight.integer_def"
obua@17644	486	"int_sub_th" > "HOLLight.hollight.int_sub_th"
obua@17644	487	"int_sub_def" > "HOLLight.hollight.int_sub_def"
kaliszyk@44639	488	"int_sgn_th" > "HOLLight.hollight.int_sgn_th"
kaliszyk@44639	489	"int_sgn_def" > "HOLLight.hollight.int_sgn_def"
obua@17644	490	"int_pow_th" > "HOLLight.hollight.int_pow_th"
obua@17644	491	"int_pow_def" > "HOLLight.hollight.int_pow_def"
obua@17644	492	"int_of_num_th" > "HOLLight.hollight.int_of_num_th"
obua@17644	493	"int_of_num_def" > "HOLLight.hollight.int_of_num_def"
obua@17644	494	"int_neg_th" > "HOLLight.hollight.int_neg_th"
obua@17644	495	"int_neg_def" > "HOLLight.hollight.int_neg_def"
obua@17644	496	"int_mul_th" > "HOLLight.hollight.int_mul_th"
obua@17644	497	"int_mul_def" > "HOLLight.hollight.int_mul_def"
kaliszyk@44639	498	"int_mod_def" > "HOLLight.hollight.int_mod_def"
obua@17644	499	"int_min_th" > "HOLLight.hollight.int_min_th"
obua@17644	500	"int_min_def" > "HOLLight.hollight.int_min_def"
obua@17644	501	"int_max_th" > "HOLLight.hollight.int_max_th"
obua@17644	502	"int_max_def" > "HOLLight.hollight.int_max_def"
obua@17644	503	"int_lt_def" > "HOLLight.hollight.int_lt_def"
obua@17644	504	"int_le_def" > "HOLLight.hollight.int_le_def"
obua@17644	505	"int_gt_def" > "HOLLight.hollight.int_gt_def"
obua@17644	506	"int_ge_def" > "HOLLight.hollight.int_ge_def"
kaliszyk@44639	507	"int_gcd_def" > "HOLLight.hollight.int_gcd_def"
kaliszyk@44639	508	"int_eq" > "HOLLight.hollight.int.real_of_int_inject"
kaliszyk@44639	509	"int_divides_def" > "HOLLight.hollight.int_divides_def"
kaliszyk@44639	510	"int_coprime_def" > "HOLLight.hollight.int_coprime_def"
kaliszyk@44639	511	"int_congruent" > "HOLLight.hollight.int_congruent"
obua@17644	512	"int_add_th" > "HOLLight.hollight.int_add_th"
obua@17644	513	"int_add_def" > "HOLLight.hollight.int_add_def"
obua@17644	514	"int_abs_th" > "HOLLight.hollight.int_abs_th"
obua@17644	515	"int_abs_def" > "HOLLight.hollight.int_abs_def"
obua@17644	516	"hreal_of_num_def" > "HOLLight.hollight.hreal_of_num_def"
obua@17644	517	"hreal_mul_def" > "HOLLight.hollight.hreal_mul_def"
obua@17644	518	"hreal_le_def" > "HOLLight.hollight.hreal_le_def"
obua@17644	519	"hreal_inv_def" > "HOLLight.hollight.hreal_inv_def"
obua@17644	520	"hreal_add_def" > "HOLLight.hollight.hreal_add_def"
obua@17644	521	"fstcart_def" > "HOLLight.hollight.fstcart_def"
obua@17644	522	"eqeq_def" > "HOLLight.hollight.eqeq_def"
kaliszyk@44639	523	"elemma0" > "HOLLight.hollight.elemma0"
kaliszyk@44639	524	"div_def" > "HOLLight.hollight.div_def"
obua@17644	525	"dist_def" > "HOLLight.hollight.dist_def"
obua@17644	526	"dimindex_def" > "HOLLight.hollight.dimindex_def"
obua@17644	527	"dest_int_rep" > "HOLLight.hollight.dest_int_rep"
obua@17644	528	"cth" > "HOLLight.hollight.cth"
obua@19093	529	"bool_RECURSION" > "HOLLight.hollight.bool_RECURSION"
kaliszyk@44639	530	"bool_INDUCT" > "Product_Type.bool.induct"
obua@17644	531	"ax__3" > "HOL4Setup.INFINITY_AX"
kaliszyk@44639	532	"ax__2" > "Hilbert_Choice.someI"
kaliszyk@44639	533	"ax__1" > "HOL.eta_contract_eq"
obua@17644	534	"admissible_def" > "HOLLight.hollight.admissible_def"
kaliszyk@44639	535	"_UNGUARDED_PATTERN_def" > "HOLLight.hollight._UNGUARDED_PATTERN_def"
kaliszyk@44639	536	"_SEQPATTERN_def" > "HOLLight.hollight._SEQPATTERN_def"
kaliszyk@44639	537	"_MATCH_def" > "HOLLight.hollight._MATCH_def"
kaliszyk@44639	538	"_GUARDED_PATTERN_def" > "HOLLight.hollight._GUARDED_PATTERN_def"
kaliszyk@44639	539	"_FUNCTION_def" > "HOLLight.hollight._FUNCTION_def"
obua@17644	540	"_FALSITY__def" > "HOLLight.hollight._FALSITY__def"
kaliszyk@44639	541	"_11937_def" > "HOLLight.hollight._11937_def"
obua@17644	542	"ZRECSPACE_def" > "HOLLight.hollight.ZRECSPACE_def"
kaliszyk@44639	543	"ZIP" > "HOLLightList.ZIP"
obua@17644	544	"ZCONSTR_def" > "HOLLight.hollight.ZCONSTR_def"
obua@17644	545	"ZCONSTR_ZBOT" > "HOLLight.hollight.ZCONSTR_ZBOT"
obua@17644	546	"ZBOT_def" > "HOLLight.hollight.ZBOT_def"
obua@17644	547	"WLOG_LT" > "HOLLight.hollight.WLOG_LT"
obua@17644	548	"WLOG_LE" > "HOLLight.hollight.WLOG_LE"
obua@17644	549	"WF_num" > "HOLLight.hollight.WF_num"
obua@17644	550	"WF_UREC_WF" > "HOLLight.hollight.WF_UREC_WF"
obua@17644	551	"WF_UREC" > "HOLLight.hollight.WF_UREC"
obua@17644	552	"WF_SUBSET" > "HOLLight.hollight.WF_SUBSET"
obua@17644	553	"WF_REFL" > "HOLLight.hollight.WF_REFL"
obua@17644	554	"WF_REC_num" > "HOLLight.hollight.WF_REC_num"
obua@17644	555	"WF_REC_WF" > "HOLLight.hollight.WF_REC_WF"
obua@17644	556	"WF_REC_TAIL_GENERAL" > "HOLLight.hollight.WF_REC_TAIL_GENERAL"
obua@17644	557	"WF_REC_TAIL" > "HOLLight.hollight.WF_REC_TAIL"
obua@17644	558	"WF_REC_INVARIANT" > "HOLLight.hollight.WF_REC_INVARIANT"
obua@17644	559	"WF_REC" > "HOLLight.hollight.WF_REC"
obua@17644	560	"WF_POINTWISE" > "HOLLight.hollight.WF_POINTWISE"
obua@17644	561	"WF_MEASURE_GEN" > "HOLLight.hollight.WF_MEASURE_GEN"
obua@17644	562	"WF_MEASURE" > "HOLLight.hollight.WF_MEASURE"
obua@17644	563	"WF_LEX_DEPENDENT" > "HOLLight.hollight.WF_LEX_DEPENDENT"
obua@17644	564	"WF_LEX" > "HOLLight.hollight.WF_LEX"
kaliszyk@44639	565	"WF_INT_MEASURE_2" > "HOLLight.hollight.WF_INT_MEASURE_2"
kaliszyk@44639	566	"WF_INT_MEASURE" > "HOLLight.hollight.WF_INT_MEASURE"
obua@17644	567	"WF_IND" > "HOLLight.hollight.WF_IND"
kaliszyk@44639	568	"WF_FINITE" > "HOLLight.hollight.WF_FINITE"
kaliszyk@44639	569	"WF_FALSE" > "Wellfounded.wfP_empty"
obua@17644	570	"WF_EREC" > "HOLLight.hollight.WF_EREC"
obua@17644	571	"WF_EQ" > "HOLLight.hollight.WF_EQ"
obua@17644	572	"WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
obua@17644	573	"UNWIND_THM2" > "HOL.simp_thms_39"
obua@17644	574	"UNWIND_THM1" > "HOL.simp_thms_40"
kaliszyk@44714	575	"UNIV_SUBSET" > "Orderings.top_class.top_unique"
kaliszyk@44639	576	"UNIV_NOT_EMPTY" > "Set.UNIV_not_empty"
obua@17644	577	"UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
obua@17644	578	"UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
obua@17644	579	"UNION_UNIV" > "HOLLight.hollight.UNION_UNIV"
kaliszyk@44639	580	"UNION_SUBSET" > "Lattices.semilattice_sup_class.le_sup_iff"
kaliszyk@44639	581	"UNION_OVER_INTER" > "Lattices.distrib_lattice_class.distrib_3"
kaliszyk@44639	582	"UNION_IDEMPOT" > "Big_Operators.lattice_class.Sup_fin.idem"
obua@17644	583	"UNION_EMPTY" > "HOLLight.hollight.UNION_EMPTY"
kaliszyk@44639	584	"UNION_COMM" > "Lattices.lattice_class.inf_sup_aci_5"
kaliszyk@44639	585	"UNION_ASSOC" > "Lattices.lattice_class.inf_sup_aci_6"
obua@17644	586	"UNION_ACI" > "HOLLight.hollight.UNION_ACI"
kaliszyk@44639	587	"UNIONS_UNION" > "Complete_Lattice.Union_Un_distrib"
kaliszyk@44639	588	"UNIONS_SUBSET" > "HOLLight.hollight.UNIONS_SUBSET"
kaliszyk@44639	589	"UNIONS_INTERS" > "HOLLight.hollight.UNIONS_INTERS"
kaliszyk@44639	590	"UNIONS_INSERT" > "Complete_Lattice.Union_insert"
kaliszyk@44639	591	"UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
kaliszyk@44639	592	"UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
kaliszyk@44639	593	"UNIONS_2" > "Complete_Lattice.Un_eq_Union"
kaliszyk@44639	594	"UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
kaliszyk@44639	595	"UNIONS_0" > "Complete_Lattice.Union_empty"
obua@17644	596	"UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
obua@17644	597	"TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
obua@17644	598	"TYDEF_real" > "HOLLight.hollight.TYDEF_real"
obua@17644	599	"TYDEF_nadd" > "HOLLight.hollight.TYDEF_nadd"
obua@17644	600	"TYDEF_int" > "HOLLight.hollight.TYDEF_int"
obua@17644	601	"TYDEF_hreal" > "HOLLight.hollight.TYDEF_hreal"
obua@17644	602	"TYDEF_finite_sum" > "HOLLight.hollight.TYDEF_finite_sum"
obua@17644	603	"TYDEF_finite_image" > "HOLLight.hollight.TYDEF_finite_image"
kaliszyk@44639	604	"TYDEF_char" > "HOLLight.hollight.TYDEF_char"
obua@17644	605	"TYDEF_cart" > "HOLLight.hollight.TYDEF_cart"
obua@17644	606	"TYDEF_3" > "HOLLight.hollight.TYDEF_3"
obua@17644	607	"TYDEF_2" > "HOLLight.hollight.TYDEF_2"
obua@17644	608	"TWO" > "HOLLight.hollight.TWO"
obua@17644	609	"TRIV_OR_FORALL_THM" > "HOLLight.hollight.TRIV_OR_FORALL_THM"
obua@17644	610	"TRIV_FORALL_OR_THM" > "HOLLight.hollight.TRIV_FORALL_OR_THM"
obua@17644	611	"TRIV_FORALL_IMP_THM" > "HOLLight.hollight.TRIV_FORALL_IMP_THM"
obua@17644	612	"TRIV_EXISTS_IMP_THM" > "HOLLight.hollight.TRIV_EXISTS_IMP_THM"
obua@17644	613	"TRIV_EXISTS_AND_THM" > "HOLLight.hollight.TRIV_EXISTS_AND_THM"
obua@17644	614	"TRIV_AND_EXISTS_THM" > "HOLLight.hollight.TRIV_AND_EXISTS_THM"
obua@17644	615	"TREAL_OF_NUM_WELLDEF" > "HOLLight.hollight.TREAL_OF_NUM_WELLDEF"
obua@17644	616	"TREAL_OF_NUM_MUL" > "HOLLight.hollight.TREAL_OF_NUM_MUL"
obua@17644	617	"TREAL_OF_NUM_LE" > "HOLLight.hollight.TREAL_OF_NUM_LE"
obua@17644	618	"TREAL_OF_NUM_EQ" > "HOLLight.hollight.TREAL_OF_NUM_EQ"
obua@17644	619	"TREAL_OF_NUM_ADD" > "HOLLight.hollight.TREAL_OF_NUM_ADD"
obua@17644	620	"TREAL_NEG_WELLDEF" > "HOLLight.hollight.TREAL_NEG_WELLDEF"
obua@17644	621	"TREAL_MUL_WELLDEFR" > "HOLLight.hollight.TREAL_MUL_WELLDEFR"
obua@17644	622	"TREAL_MUL_WELLDEF" > "HOLLight.hollight.TREAL_MUL_WELLDEF"
obua@17644	623	"TREAL_MUL_SYM_EQ" > "HOLLight.hollight.TREAL_MUL_SYM_EQ"
obua@17644	624	"TREAL_MUL_SYM" > "HOLLight.hollight.TREAL_MUL_SYM"
obua@17644	625	"TREAL_MUL_LINV" > "HOLLight.hollight.TREAL_MUL_LINV"
obua@17644	626	"TREAL_MUL_LID" > "HOLLight.hollight.TREAL_MUL_LID"
obua@17644	627	"TREAL_MUL_ASSOC" > "HOLLight.hollight.TREAL_MUL_ASSOC"
obua@17644	628	"TREAL_LE_WELLDEF" > "HOLLight.hollight.TREAL_LE_WELLDEF"
obua@17644	629	"TREAL_LE_TRANS" > "HOLLight.hollight.TREAL_LE_TRANS"
obua@17644	630	"TREAL_LE_TOTAL" > "HOLLight.hollight.TREAL_LE_TOTAL"
obua@17644	631	"TREAL_LE_REFL" > "HOLLight.hollight.TREAL_LE_REFL"
obua@17644	632	"TREAL_LE_MUL" > "HOLLight.hollight.TREAL_LE_MUL"
obua@17644	633	"TREAL_LE_LADD_IMP" > "HOLLight.hollight.TREAL_LE_LADD_IMP"
obua@17644	634	"TREAL_LE_ANTISYM" > "HOLLight.hollight.TREAL_LE_ANTISYM"
obua@17644	635	"TREAL_INV_WELLDEF" > "HOLLight.hollight.TREAL_INV_WELLDEF"
obua@17644	636	"TREAL_INV_0" > "HOLLight.hollight.TREAL_INV_0"
obua@17644	637	"TREAL_EQ_TRANS" > "HOLLight.hollight.TREAL_EQ_TRANS"
obua@17644	638	"TREAL_EQ_SYM" > "HOLLight.hollight.TREAL_EQ_SYM"
obua@17644	639	"TREAL_EQ_REFL" > "HOLLight.hollight.TREAL_EQ_REFL"
obua@17644	640	"TREAL_EQ_IMP_LE" > "HOLLight.hollight.TREAL_EQ_IMP_LE"
obua@17644	641	"TREAL_EQ_AP" > "HOLLight.hollight.TREAL_EQ_AP"
obua@17644	642	"TREAL_ADD_WELLDEFR" > "HOLLight.hollight.TREAL_ADD_WELLDEFR"
obua@17644	643	"TREAL_ADD_WELLDEF" > "HOLLight.hollight.TREAL_ADD_WELLDEF"
obua@17644	644	"TREAL_ADD_SYM_EQ" > "HOLLight.hollight.TREAL_ADD_SYM_EQ"
obua@17644	645	"TREAL_ADD_SYM" > "HOLLight.hollight.TREAL_ADD_SYM"
obua@17644	646	"TREAL_ADD_LINV" > "HOLLight.hollight.TREAL_ADD_LINV"
obua@17644	647	"TREAL_ADD_LID" > "HOLLight.hollight.TREAL_ADD_LID"
obua@17644	648	"TREAL_ADD_LDISTRIB" > "HOLLight.hollight.TREAL_ADD_LDISTRIB"
obua@17644	649	"TREAL_ADD_ASSOC" > "HOLLight.hollight.TREAL_ADD_ASSOC"
kaliszyk@44639	650	"TRANSITIVE_STEPWISE_LT_EQ" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LT_EQ"
kaliszyk@44639	651	"TRANSITIVE_STEPWISE_LT" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LT"
kaliszyk@44639	652	"TRANSITIVE_STEPWISE_LE_EQ" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LE_EQ"
kaliszyk@44639	653	"TRANSITIVE_STEPWISE_LE" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LE"
kaliszyk@44639	654	"TOPOLOGICAL_SORT" > "HOLLight.hollight.TOPOLOGICAL_SORT"
kaliszyk@44639	655	"SWAP_FORALL_THM" > "HOL.all_comm"
kaliszyk@44639	656	"SWAP_EXISTS_THM" > "HOL.ex_comm"
obua@17644	657	"SURJ_def" > "HOLLight.hollight.SURJ_def"
obua@17644	658	"SURJECTIVE_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_RIGHT_INVERSE"
obua@17644	659	"SURJECTIVE_ON_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_ON_RIGHT_INVERSE"
kaliszyk@44639	660	"SURJECTIVE_ON_IMAGE" > "HOLLight.hollight.SURJECTIVE_ON_IMAGE"
kaliszyk@44639	661	"SURJECTIVE_MAP" > "HOLLightList.SURJECTIVE_MAP"
kaliszyk@44639	662	"SURJECTIVE_IMAGE_THM" > "HOLLight.hollight.SURJECTIVE_IMAGE_THM"
kaliszyk@44639	663	"SURJECTIVE_IMAGE_EQ" > "HOLLight.hollight.SURJECTIVE_IMAGE_EQ"
kaliszyk@44639	664	"SURJECTIVE_IMAGE" > "HOLLight.hollight.SURJECTIVE_IMAGE"
obua@17644	665	"SURJECTIVE_IFF_INJECTIVE_GEN" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE_GEN"
obua@17644	666	"SURJECTIVE_IFF_INJECTIVE" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE"
kaliszyk@44639	667	"SURJECTIVE_FORALL_THM" > "HOLLight.hollight.SURJECTIVE_FORALL_THM"
kaliszyk@44639	668	"SURJECTIVE_EXISTS_THM" > "HOLLight.hollight.SURJECTIVE_EXISTS_THM"
obua@17644	669	"SUPPORT_SUPPORT" > "HOLLight.hollight.SUPPORT_SUPPORT"
obua@17644	670	"SUPPORT_SUBSET" > "HOLLight.hollight.SUPPORT_SUBSET"
obua@17644	671	"SUPPORT_EMPTY" > "HOLLight.hollight.SUPPORT_EMPTY"
obua@17644	672	"SUPPORT_DELTA" > "HOLLight.hollight.SUPPORT_DELTA"
obua@17644	673	"SUPPORT_CLAUSES" > "HOLLight.hollight.SUPPORT_CLAUSES"
kaliszyk@44639	674	"SUPERADMISSIBLE_TAIL" > "HOLLight.hollight.SUPERADMISSIBLE_TAIL"
obua@17644	675	"SUPERADMISSIBLE_T" > "HOLLight.hollight.SUPERADMISSIBLE_T"
kaliszyk@44639	676	"SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN"
kaliszyk@44639	677	"SUPERADMISSIBLE_MATCH_SEQPATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_SEQPATTERN"
kaliszyk@44639	678	"SUPERADMISSIBLE_MATCH_GUARDED_PATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_GUARDED_PATTERN"
kaliszyk@44639	679	"SUPERADMISSIBLE_CONST" > "HOLLight.hollight.SUPERADMISSIBLE_CONST"
obua@17644	680	"SUPERADMISSIBLE_COND" > "HOLLight.hollight.SUPERADMISSIBLE_COND"
kaliszyk@44639	681	"SUM_ZERO_EXISTS" > "HOLLight.hollight.SUM_ZERO_EXISTS"
obua@17644	682	"SUM_UNION_RZERO" > "HOLLight.hollight.SUM_UNION_RZERO"
kaliszyk@44639	683	"SUM_UNION_NONZERO" > "HOLLight.hollight.SUM_UNION_NONZERO"
obua@17644	684	"SUM_UNION_LZERO" > "HOLLight.hollight.SUM_UNION_LZERO"
obua@17644	685	"SUM_UNION_EQ" > "HOLLight.hollight.SUM_UNION_EQ"
kaliszyk@44639	686	"SUM_UNIONS_NONZERO" > "HOLLight.hollight.SUM_UNIONS_NONZERO"
obua@17644	687	"SUM_UNION" > "HOLLight.hollight.SUM_UNION"
obua@17644	688	"SUM_TRIV_NUMSEG" > "HOLLight.hollight.SUM_TRIV_NUMSEG"
obua@17644	689	"SUM_SWAP_NUMSEG" > "HOLLight.hollight.SUM_SWAP_NUMSEG"
obua@17644	690	"SUM_SWAP" > "HOLLight.hollight.SUM_SWAP"
obua@17644	691	"SUM_SUPPORT" > "HOLLight.hollight.SUM_SUPPORT"
obua@17644	692	"SUM_SUPERSET" > "HOLLight.hollight.SUM_SUPERSET"
obua@17644	693	"SUM_SUM_RESTRICT" > "HOLLight.hollight.SUM_SUM_RESTRICT"
obua@19093	694	"SUM_SUM_PRODUCT" > "HOLLight.hollight.SUM_SUM_PRODUCT"
obua@17644	695	"SUM_SUB_NUMSEG" > "HOLLight.hollight.SUM_SUB_NUMSEG"
obua@17644	696	"SUM_SUBSET_SIMPLE" > "HOLLight.hollight.SUM_SUBSET_SIMPLE"
obua@17644	697	"SUM_SUBSET" > "HOLLight.hollight.SUM_SUBSET"
obua@17644	698	"SUM_SUB" > "HOLLight.hollight.SUM_SUB"
obua@17644	699	"SUM_SING_NUMSEG" > "HOLLight.hollight.SUM_SING_NUMSEG"
obua@17644	700	"SUM_SING" > "HOLLight.hollight.SUM_SING"
kaliszyk@44639	701	"SUM_RMUL" > "HOLLight.hollight.SUM_RMUL"
obua@17644	702	"SUM_RESTRICT_SET" > "HOLLight.hollight.SUM_RESTRICT_SET"
obua@17644	703	"SUM_RESTRICT" > "HOLLight.hollight.SUM_RESTRICT"
obua@17644	704	"SUM_POS_LE_NUMSEG" > "HOLLight.hollight.SUM_POS_LE_NUMSEG"
obua@17644	705	"SUM_POS_LE" > "HOLLight.hollight.SUM_POS_LE"
obua@17644	706	"SUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_POS_EQ_0_NUMSEG"
obua@17644	707	"SUM_POS_EQ_0" > "HOLLight.hollight.SUM_POS_EQ_0"
obua@17644	708	"SUM_POS_BOUND" > "HOLLight.hollight.SUM_POS_BOUND"
kaliszyk@44639	709	"SUM_PARTIAL_SUC" > "HOLLight.hollight.SUM_PARTIAL_SUC"
kaliszyk@44639	710	"SUM_PARTIAL_PRE" > "HOLLight.hollight.SUM_PARTIAL_PRE"
kaliszyk@44639	711	"SUM_PAIR" > "HOLLight.hollight.SUM_PAIR"
obua@17644	712	"SUM_OFFSET_0" > "HOLLight.hollight.SUM_OFFSET_0"
obua@17644	713	"SUM_OFFSET" > "HOLLight.hollight.SUM_OFFSET"
obua@17644	714	"SUM_NEG" > "HOLLight.hollight.SUM_NEG"
obua@17644	715	"SUM_MULTICOUNT_GEN" > "HOLLight.hollight.SUM_MULTICOUNT_GEN"
obua@17644	716	"SUM_MULTICOUNT" > "HOLLight.hollight.SUM_MULTICOUNT"
obua@17644	717	"SUM_LT_ALL" > "HOLLight.hollight.SUM_LT_ALL"
obua@17644	718	"SUM_LT" > "HOLLight.hollight.SUM_LT"
kaliszyk@44639	719	"SUM_LMUL" > "HOLLight.hollight.SUM_LMUL"
obua@17644	720	"SUM_LE_NUMSEG" > "HOLLight.hollight.SUM_LE_NUMSEG"
kaliszyk@44639	721	"SUM_LE_INCLUDED" > "HOLLight.hollight.SUM_LE_INCLUDED"
obua@17644	722	"SUM_LE" > "HOLLight.hollight.SUM_LE"
kaliszyk@44639	723	"SUM_INJECTION" > "HOLLight.hollight.SUM_INJECTION"
kaliszyk@44639	724	"SUM_INCL_EXCL" > "HOLLight.hollight.SUM_INCL_EXCL"
kaliszyk@44639	725	"SUM_IMAGE_NONZERO" > "HOLLight.hollight.SUM_IMAGE_NONZERO"
kaliszyk@44639	726	"SUM_IMAGE_LE" > "HOLLight.hollight.SUM_IMAGE_LE"
obua@17644	727	"SUM_IMAGE_GEN" > "HOLLight.hollight.SUM_IMAGE_GEN"
obua@17644	728	"SUM_IMAGE" > "HOLLight.hollight.SUM_IMAGE"
kaliszyk@44639	729	"SUM_GROUP" > "HOLLight.hollight.SUM_GROUP"
obua@17644	730	"SUM_EQ_SUPERSET" > "HOLLight.hollight.SUM_EQ_SUPERSET"
obua@17644	731	"SUM_EQ_NUMSEG" > "HOLLight.hollight.SUM_EQ_NUMSEG"
kaliszyk@44639	732	"SUM_EQ_GENERAL_INVERSES" > "HOLLight.hollight.SUM_EQ_GENERAL_INVERSES"
obua@19093	733	"SUM_EQ_GENERAL" > "HOLLight.hollight.SUM_EQ_GENERAL"
obua@17644	734	"SUM_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_EQ_0_NUMSEG"
obua@17644	735	"SUM_EQ_0" > "HOLLight.hollight.SUM_EQ_0"
obua@17644	736	"SUM_EQ" > "HOLLight.hollight.SUM_EQ"
kaliszyk@44639	737	"SUM_DIFFS_ALT" > "HOLLight.hollight.SUM_DIFFS_ALT"
kaliszyk@44639	738	"SUM_DIFFS" > "HOLLight.hollight.SUM_DIFFS"
obua@17644	739	"SUM_DIFF" > "HOLLight.hollight.SUM_DIFF"
obua@17644	740	"SUM_DELTA" > "HOLLight.hollight.SUM_DELTA"
kaliszyk@44639	741	"SUM_DELETE_CASES" > "HOLLight.hollight.SUM_DELETE_CASES"
kaliszyk@44639	742	"SUM_DELETE" > "HOLLight.hollight.SUM_DELETE"
obua@17644	743	"SUM_CONST_NUMSEG" > "HOLLight.hollight.SUM_CONST_NUMSEG"
obua@17644	744	"SUM_CONST" > "HOLLight.hollight.SUM_CONST"
kaliszyk@44639	745	"SUM_COMBINE_R" > "HOLLight.hollight.SUM_COMBINE_R"
kaliszyk@44639	746	"SUM_COMBINE_L" > "HOLLight.hollight.SUM_COMBINE_L"
kaliszyk@44639	747	"SUM_CLOSED" > "HOLLight.hollight.SUM_CLOSED"
obua@17644	748	"SUM_CLAUSES_RIGHT" > "HOLLight.hollight.SUM_CLAUSES_RIGHT"
obua@17644	749	"SUM_CLAUSES_NUMSEG" > "HOLLight.hollight.SUM_CLAUSES_NUMSEG"
obua@17644	750	"SUM_CLAUSES_LEFT" > "HOLLight.hollight.SUM_CLAUSES_LEFT"
obua@17644	751	"SUM_CLAUSES" > "HOLLight.hollight.SUM_CLAUSES"
kaliszyk@44639	752	"SUM_CASES_1" > "HOLLight.hollight.SUM_CASES_1"
kaliszyk@44639	753	"SUM_CASES" > "HOLLight.hollight.SUM_CASES"
obua@17644	754	"SUM_BOUND_LT_GEN" > "HOLLight.hollight.SUM_BOUND_LT_GEN"
obua@17644	755	"SUM_BOUND_LT_ALL" > "HOLLight.hollight.SUM_BOUND_LT_ALL"
obua@17644	756	"SUM_BOUND_LT" > "HOLLight.hollight.SUM_BOUND_LT"
obua@17644	757	"SUM_BOUND_GEN" > "HOLLight.hollight.SUM_BOUND_GEN"
obua@17644	758	"SUM_BOUND" > "HOLLight.hollight.SUM_BOUND"
obua@19093	759	"SUM_BIJECTION" > "HOLLight.hollight.SUM_BIJECTION"
obua@17644	760	"SUM_ADD_SPLIT" > "HOLLight.hollight.SUM_ADD_SPLIT"
obua@17644	761	"SUM_ADD_NUMSEG" > "HOLLight.hollight.SUM_ADD_NUMSEG"
kaliszyk@44639	762	"SUM_ADD_GEN" > "HOLLight.hollight.SUM_ADD_GEN"
obua@17644	763	"SUM_ADD" > "HOLLight.hollight.SUM_ADD"
obua@17644	764	"SUM_ABS_NUMSEG" > "HOLLight.hollight.SUM_ABS_NUMSEG"
kaliszyk@44639	765	"SUM_ABS_LE" > "HOLLight.hollight.SUM_ABS_LE"
obua@17644	766	"SUM_ABS_BOUND" > "HOLLight.hollight.SUM_ABS_BOUND"
obua@17644	767	"SUM_ABS" > "HOLLight.hollight.SUM_ABS"
obua@17644	768	"SUM_0" > "HOLLight.hollight.SUM_0"
kaliszyk@44639	769	"SUC_SUB1" > "Nat.diff_Suc_1"
kaliszyk@44639	770	"SUC_INJ" > "HOLLightCompat.SUC_INJ"
obua@17644	771	"SUB_SUC" > "Nat.diff_Suc_Suc"
obua@17644	772	"SUB_REFL" > "Nat.diff_self_eq_0"
obua@17644	773	"SUB_PRESUC" > "HOLLight.hollight.SUB_PRESUC"
kaliszyk@44639	774	"SUB_EQ_0" > "Nat.diff_is_0_eq"
obua@17644	775	"SUB_ELIM_THM" > "HOLLight.hollight.SUB_ELIM_THM"
obua@17644	776	"SUB_ADD_RCANCEL" > "Nat.diff_cancel2"
obua@17644	777	"SUB_ADD_LCANCEL" > "Nat.diff_cancel"
kaliszyk@44639	778	"SUB_ADD" > "Nat.le_add_diff_inverse2"
obua@17644	779	"SUB_0" > "HOLLight.hollight.SUB_0"
kaliszyk@44639	780	"SUBSET_UNIV" > "Orderings.top_class.top_greatest"
kaliszyk@44639	781	"SUBSET_UNION_ABSORPTION" > "Lattices.semilattice_sup_class.le_iff_sup"
kaliszyk@44639	782	"SUBSET_UNIONS" > "Complete_Lattice.Union_mono"
obua@17644	783	"SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
kaliszyk@44639	784	"SUBSET_TRANS" > "Orderings.order_trans_rules_23"
obua@17644	785	"SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
kaliszyk@44639	786	"SUBSET_REFL" > "Inductive.basic_monos_1"
kaliszyk@44639	787	"SUBSET_PSUBSET_TRANS" > "Orderings.order_le_less_trans"
obua@17644	788	"SUBSET_NUMSEG" > "HOLLight.hollight.SUBSET_NUMSEG"
kaliszyk@44639	789	"SUBSET_INTER_ABSORPTION" > "Lattices.semilattice_inf_class.le_iff_inf"
kaliszyk@44639	790	"SUBSET_INTER" > "Lattices.semilattice_inf_class.le_inf_iff"
obua@17644	791	"SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
kaliszyk@44639	792	"SUBSET_INSERT" > "Set.subset_insert"
kaliszyk@44639	793	"SUBSET_IMAGE" > "Set.subset_image_iff"
kaliszyk@44714	794	"SUBSET_EMPTY" > "Orderings.bot_class.bot_unique"
kaliszyk@44639	795	"SUBSET_DIFF" > "Set.Diff_subset"
obua@17644	796	"SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
kaliszyk@44639	797	"SUBSET_CARD_EQ" > "HOLLight.hollight.SUBSET_CARD_EQ"
kaliszyk@44639	798	"SUBSET_ANTISYM_EQ" > "Orderings.order_class.eq_iff"
kaliszyk@44639	799	"SUBSET_ANTISYM" > "Orderings.order_antisym"
obua@17644	800	"SND" > "Product_Type.snd_conv"
obua@17644	801	"SKOLEM_THM" > "HOLLight.hollight.SKOLEM_THM"
obua@17644	802	"SING_def" > "HOLLight.hollight.SING_def"
kaliszyk@44639	803	"SING_SUBSET" > "HOLLight.hollight.SING_SUBSET"
kaliszyk@44639	804	"SING_GSPEC" > "HOLLight.hollight.SING_GSPEC"
kaliszyk@44639	805	"SIMPLE_IMAGE_GEN" > "HOLLight.hollight.SIMPLE_IMAGE_GEN"
obua@17644	806	"SIMPLE_IMAGE" > "HOLLight.hollight.SIMPLE_IMAGE"
obua@17644	807	"SET_RECURSION_LEMMA" > "HOLLight.hollight.SET_RECURSION_LEMMA"
kaliszyk@44639	808	"SET_PROVE_CASES" > "HOLLight.hollight.SET_PROVE_CASES"
kaliszyk@44639	809	"SET_PAIR_THM" > "HOLLight.hollight.SET_PAIR_THM"
kaliszyk@44639	810	"SET_OF_LIST_MAP" > "List.set_map"
kaliszyk@44639	811	"SET_OF_LIST_EQ_EMPTY" > "List.set_empty"
kaliszyk@44639	812	"SET_OF_LIST_APPEND" > "List.set_append"
obua@17644	813	"SET_CASES" > "HOLLight.hollight.SET_CASES"
obua@17644	814	"SEMIRING_PTHS" > "HOLLight.hollight.SEMIRING_PTHS"
obua@17644	815	"SELECT_UNIQUE" > "HOLLight.hollight.SELECT_UNIQUE"
obua@17644	816	"SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
obua@17644	817	"SELECT_LEMMA" > "Hilbert_Choice.some_sym_eq_trivial"
kaliszyk@44639	818	"RIGHT_SUB_DISTRIB" > "Nat.diff_mult_distrib"
obua@17644	819	"RIGHT_OR_FORALL_THM" > "HOL.all_simps_4"
obua@17644	820	"RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
kaliszyk@44639	821	"RIGHT_OR_DISTRIB" > "Groebner_Basis.dnf_2"
obua@17644	822	"RIGHT_IMP_FORALL_THM" > "HOL.all_simps_6"
obua@17644	823	"RIGHT_IMP_EXISTS_THM" > "HOL.ex_simps_6"
obua@17644	824	"RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
obua@17644	825	"RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
obua@17644	826	"RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
obua@17644	827	"RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
obua@17644	828	"RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
obua@17644	829	"RIGHT_AND_EXISTS_THM" > "HOL.ex_simps_2"
kaliszyk@44639	830	"RIGHT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_26"
kaliszyk@44639	831	"REVERSE_REVERSE" > "List.rev_rev_ident"
kaliszyk@44639	832	"REVERSE_APPEND" > "List.rev_append"
obua@17644	833	"REST_def" > "HOLLight.hollight.REST_def"
kaliszyk@44639	834	"REFL_CLAUSE" > "Groebner_Basis.bool_simps_6"
obua@17644	835	"REAL_WLOG_LT" > "HOLLight.hollight.REAL_WLOG_LT"
obua@17644	836	"REAL_WLOG_LE" > "HOLLight.hollight.REAL_WLOG_LE"
obua@17644	837	"REAL_SUB_TRIANGLE" > "HOLLight.hollight.REAL_SUB_TRIANGLE"
obua@17644	838	"REAL_SUB_SUB2" > "HOLLight.hollight.REAL_SUB_SUB2"
obua@17644	839	"REAL_SUB_SUB" > "HOLLight.hollight.REAL_SUB_SUB"
obua@17644	840	"REAL_SUB_RZERO" > "HOLLight.hollight.REAL_SUB_RZERO"
obua@17644	841	"REAL_SUB_RNEG" > "HOLLight.hollight.REAL_SUB_RNEG"
obua@17644	842	"REAL_SUB_REFL" > "HOLLight.hollight.REAL_SUB_REFL"
obua@17644	843	"REAL_SUB_RDISTRIB" > "HOLLight.hollight.REAL_SUB_RDISTRIB"
kaliszyk@44639	844	"REAL_SUB_POW_R1" > "HOLLight.hollight.REAL_SUB_POW_R1"
kaliszyk@44639	845	"REAL_SUB_POW_L1" > "HOLLight.hollight.REAL_SUB_POW_L1"
kaliszyk@44639	846	"REAL_SUB_POW" > "HOLLight.hollight.REAL_SUB_POW"
obua@17644	847	"REAL_SUB_NEG2" > "HOLLight.hollight.REAL_SUB_NEG2"
obua@17644	848	"REAL_SUB_LZERO" > "HOLLight.hollight.REAL_SUB_LZERO"
obua@17644	849	"REAL_SUB_LT" > "HOLLight.hollight.REAL_SUB_LT"
obua@17644	850	"REAL_SUB_LNEG" > "HOLLight.hollight.REAL_SUB_LNEG"
obua@17644	851	"REAL_SUB_LE" > "HOLLight.hollight.REAL_SUB_LE"
obua@17644	852	"REAL_SUB_LDISTRIB" > "HOLLight.hollight.REAL_SUB_LDISTRIB"
obua@17644	853	"REAL_SUB_INV" > "HOLLight.hollight.REAL_SUB_INV"
obua@17644	854	"REAL_SUB_ADD2" > "HOLLight.hollight.REAL_SUB_ADD2"
obua@17644	855	"REAL_SUB_ADD" > "HOLLight.hollight.REAL_SUB_ADD"
obua@17644	856	"REAL_SUB_ABS" > "HOLLight.hollight.REAL_SUB_ABS"
obua@17644	857	"REAL_SUB_0" > "HOLLight.hollight.REAL_SUB_0"
obua@19093	858	"REAL_SOS_EQ_0" > "HOLLight.hollight.REAL_SOS_EQ_0"
kaliszyk@44639	859	"REAL_SGN_NEG" > "HOLLight.hollight.REAL_SGN_NEG"
kaliszyk@44639	860	"REAL_SGN_MUL" > "HOLLight.hollight.REAL_SGN_MUL"
kaliszyk@44639	861	"REAL_SGN_INV" > "HOLLight.hollight.REAL_SGN_INV"
kaliszyk@44639	862	"REAL_SGN_DIV" > "HOLLight.hollight.REAL_SGN_DIV"
kaliszyk@44639	863	"REAL_SGN_ABS" > "HOLLight.hollight.REAL_SGN_ABS"
kaliszyk@44639	864	"REAL_SGN_0" > "HOLLight.hollight.REAL_SGN_0"
kaliszyk@44639	865	"REAL_SGN" > "HOLLight.hollight.REAL_SGN"
obua@17644	866	"REAL_RNEG_UNIQ" > "HOLLight.hollight.REAL_RNEG_UNIQ"
kaliszyk@44639	867	"REAL_POW_ZERO" > "HOLLight.hollight.REAL_POW_ZERO"
obua@17644	868	"REAL_POW_SUB" > "HOLLight.hollight.REAL_POW_SUB"
obua@17644	869	"REAL_POW_POW" > "HOLLight.hollight.REAL_POW_POW"
obua@17644	870	"REAL_POW_ONE" > "HOLLight.hollight.REAL_POW_ONE"
obua@17644	871	"REAL_POW_NZ" > "HOLLight.hollight.REAL_POW_NZ"
obua@17644	872	"REAL_POW_NEG" > "HOLLight.hollight.REAL_POW_NEG"
obua@17644	873	"REAL_POW_MUL" > "HOLLight.hollight.REAL_POW_MUL"
obua@17644	874	"REAL_POW_MONO_LT" > "HOLLight.hollight.REAL_POW_MONO_LT"
kaliszyk@44639	875	"REAL_POW_MONO_INV" > "HOLLight.hollight.REAL_POW_MONO_INV"
obua@17644	876	"REAL_POW_MONO" > "HOLLight.hollight.REAL_POW_MONO"
kaliszyk@44639	877	"REAL_POW_LT_1" > "HOLLight.hollight.REAL_POW_LT_1"
kaliszyk@44639	878	"REAL_POW_LT2_REV" > "HOLLight.hollight.REAL_POW_LT2_REV"
kaliszyk@44639	879	"REAL_POW_LT2_ODD_EQ" > "HOLLight.hollight.REAL_POW_LT2_ODD_EQ"
kaliszyk@44639	880	"REAL_POW_LT2_ODD" > "HOLLight.hollight.REAL_POW_LT2_ODD"
obua@17644	881	"REAL_POW_LT2" > "HOLLight.hollight.REAL_POW_LT2"
obua@17644	882	"REAL_POW_LT" > "HOLLight.hollight.REAL_POW_LT"
obua@17644	883	"REAL_POW_LE_1" > "HOLLight.hollight.REAL_POW_LE_1"
kaliszyk@44639	884	"REAL_POW_LE2_REV" > "HOLLight.hollight.REAL_POW_LE2_REV"
kaliszyk@44639	885	"REAL_POW_LE2_ODD_EQ" > "HOLLight.hollight.REAL_POW_LE2_ODD_EQ"
kaliszyk@44639	886	"REAL_POW_LE2_ODD" > "HOLLight.hollight.REAL_POW_LE2_ODD"
obua@17644	887	"REAL_POW_LE2" > "HOLLight.hollight.REAL_POW_LE2"
obua@17644	888	"REAL_POW_LE" > "HOLLight.hollight.REAL_POW_LE"
obua@17644	889	"REAL_POW_INV" > "HOLLight.hollight.REAL_POW_INV"
kaliszyk@44639	890	"REAL_POW_EQ_ODD_EQ" > "HOLLight.hollight.REAL_POW_EQ_ODD_EQ"
kaliszyk@44639	891	"REAL_POW_EQ_ODD" > "HOLLight.hollight.REAL_POW_EQ_ODD"
kaliszyk@44639	892	"REAL_POW_EQ_EQ" > "HOLLight.hollight.REAL_POW_EQ_EQ"
kaliszyk@44639	893	"REAL_POW_EQ_ABS" > "HOLLight.hollight.REAL_POW_EQ_ABS"
kaliszyk@44639	894	"REAL_POW_EQ_1_IMP" > "HOLLight.hollight.REAL_POW_EQ_1_IMP"
kaliszyk@44639	895	"REAL_POW_EQ_1" > "HOLLight.hollight.REAL_POW_EQ_1"
obua@17644	896	"REAL_POW_EQ_0" > "HOLLight.hollight.REAL_POW_EQ_0"
kaliszyk@44639	897	"REAL_POW_EQ" > "HOLLight.hollight.REAL_POW_EQ"
obua@17644	898	"REAL_POW_DIV" > "HOLLight.hollight.REAL_POW_DIV"
obua@17644	899	"REAL_POW_ADD" > "HOLLight.hollight.REAL_POW_ADD"
obua@17644	900	"REAL_POW_2" > "HOLLight.hollight.REAL_POW_2"
kaliszyk@44639	901	"REAL_POW_1_LT" > "HOLLight.hollight.REAL_POW_1_LT"
obua@17644	902	"REAL_POW_1_LE" > "HOLLight.hollight.REAL_POW_1_LE"
obua@17644	903	"REAL_POW_1" > "HOLLight.hollight.REAL_POW_1"
obua@17644	904	"REAL_POW2_ABS" > "HOLLight.hollight.REAL_POW2_ABS"
obua@17644	905	"REAL_POS_NZ" > "HOLLight.hollight.REAL_POS_NZ"
obua@17644	906	"REAL_POS" > "HOLLight.hollight.REAL_POS"
obua@17644	907	"REAL_POLY_NEG_CLAUSES" > "HOLLight.hollight.REAL_POLY_NEG_CLAUSES"
obua@17644	908	"REAL_POLY_CLAUSES" > "HOLLight.hollight.REAL_POLY_CLAUSES"
obua@17644	909	"REAL_OF_NUM_SUM_NUMSEG" > "HOLLight.hollight.REAL_OF_NUM_SUM_NUMSEG"
obua@17644	910	"REAL_OF_NUM_SUM" > "HOLLight.hollight.REAL_OF_NUM_SUM"
obua@17644	911	"REAL_OF_NUM_SUC" > "HOLLight.hollight.REAL_OF_NUM_SUC"
obua@17644	912	"REAL_OF_NUM_SUB" > "HOLLight.hollight.REAL_OF_NUM_SUB"
obua@17644	913	"REAL_OF_NUM_POW" > "HOLLight.hollight.REAL_OF_NUM_POW"
kaliszyk@44639	914	"REAL_OF_NUM_MIN" > "HOLLight.hollight.REAL_OF_NUM_MIN"
kaliszyk@44639	915	"REAL_OF_NUM_MAX" > "HOLLight.hollight.REAL_OF_NUM_MAX"
obua@17644	916	"REAL_OF_NUM_LT" > "HOLLight.hollight.REAL_OF_NUM_LT"
obua@17644	917	"REAL_OF_NUM_GT" > "HOLLight.hollight.REAL_OF_NUM_GT"
obua@17644	918	"REAL_OF_NUM_GE" > "HOLLight.hollight.REAL_OF_NUM_GE"
obua@17644	919	"REAL_NOT_LT" > "HOLLight.hollight.REAL_NOT_LT"
obua@17644	920	"REAL_NOT_LE" > "HOLLight.hollight.real_lt_def"
obua@17644	921	"REAL_NOT_EQ" > "HOLLight.hollight.REAL_NOT_EQ"
obua@17644	922	"REAL_NEG_SUB" > "HOLLight.hollight.REAL_NEG_SUB"
obua@17644	923	"REAL_NEG_RMUL" > "HOLLight.hollight.REAL_NEG_RMUL"
obua@17644	924	"REAL_NEG_NEG" > "HOLLight.hollight.REAL_NEG_NEG"
obua@17644	925	"REAL_NEG_MUL2" > "HOLLight.hollight.REAL_NEG_MUL2"
obua@17644	926	"REAL_NEG_MINUS1" > "HOLLight.hollight.REAL_NEG_MINUS1"
obua@17644	927	"REAL_NEG_LT0" > "HOLLight.hollight.REAL_NEG_LT0"
obua@17644	928	"REAL_NEG_LMUL" > "HOLLight.hollight.REAL_NEG_LMUL"
obua@17644	929	"REAL_NEG_LE0" > "HOLLight.hollight.REAL_NEG_LE0"
obua@17644	930	"REAL_NEG_GT0" > "HOLLight.hollight.REAL_NEG_GT0"
obua@17644	931	"REAL_NEG_GE0" > "HOLLight.hollight.REAL_NEG_GE0"
obua@17644	932	"REAL_NEG_EQ_0" > "HOLLight.hollight.REAL_NEG_EQ_0"
obua@17644	933	"REAL_NEG_EQ" > "HOLLight.hollight.REAL_NEG_EQ"
obua@17644	934	"REAL_NEG_ADD" > "HOLLight.hollight.REAL_NEG_ADD"
obua@17644	935	"REAL_NEG_0" > "HOLLight.hollight.REAL_NEG_0"
obua@17644	936	"REAL_NEGNEG" > "HOLLight.hollight.REAL_NEGNEG"
obua@17644	937	"REAL_MUL_RZERO" > "HOLLight.hollight.REAL_MUL_RZERO"
obua@17644	938	"REAL_MUL_RNEG" > "HOLLight.hollight.REAL_MUL_RNEG"
obua@17644	939	"REAL_MUL_RINV_UNIQ" > "HOLLight.hollight.REAL_MUL_RINV_UNIQ"
obua@17644	940	"REAL_MUL_RINV" > "HOLLight.hollight.REAL_MUL_RINV"
obua@17644	941	"REAL_MUL_RID" > "HOLLight.hollight.REAL_MUL_RID"
kaliszyk@44639	942	"REAL_MUL_POS_LT" > "HOLLight.hollight.REAL_MUL_POS_LT"
kaliszyk@44639	943	"REAL_MUL_POS_LE" > "HOLLight.hollight.REAL_MUL_POS_LE"
obua@17644	944	"REAL_MUL_LZERO" > "HOLLight.hollight.REAL_MUL_LZERO"
obua@17644	945	"REAL_MUL_LNEG" > "HOLLight.hollight.REAL_MUL_LNEG"
obua@17644	946	"REAL_MUL_LINV_UNIQ" > "HOLLight.hollight.REAL_MUL_LINV_UNIQ"
obua@17644	947	"REAL_MUL_AC" > "HOLLight.hollight.REAL_MUL_AC"
obua@17644	948	"REAL_MUL_2" > "HOLLight.hollight.REAL_MUL_2"
obua@17644	949	"REAL_MIN_SYM" > "HOLLight.hollight.REAL_MIN_SYM"
obua@17644	950	"REAL_MIN_MIN" > "HOLLight.hollight.REAL_MIN_MIN"
obua@17644	951	"REAL_MIN_MAX" > "HOLLight.hollight.REAL_MIN_MAX"
obua@17644	952	"REAL_MIN_LT" > "HOLLight.hollight.REAL_MIN_LT"
obua@17644	953	"REAL_MIN_LE" > "HOLLight.hollight.REAL_MIN_LE"
obua@17644	954	"REAL_MIN_ASSOC" > "HOLLight.hollight.REAL_MIN_ASSOC"
obua@17644	955	"REAL_MIN_ACI" > "HOLLight.hollight.REAL_MIN_ACI"
obua@17644	956	"REAL_MAX_SYM" > "HOLLight.hollight.REAL_MAX_SYM"
obua@17644	957	"REAL_MAX_MIN" > "HOLLight.hollight.REAL_MAX_MIN"
obua@17644	958	"REAL_MAX_MAX" > "HOLLight.hollight.REAL_MAX_MAX"
obua@17644	959	"REAL_MAX_LT" > "HOLLight.hollight.REAL_MAX_LT"
obua@17644	960	"REAL_MAX_LE" > "HOLLight.hollight.REAL_MAX_LE"
obua@17644	961	"REAL_MAX_ASSOC" > "HOLLight.hollight.REAL_MAX_ASSOC"
obua@17644	962	"REAL_MAX_ACI" > "HOLLight.hollight.REAL_MAX_ACI"
obua@17644	963	"REAL_LT_TRANS" > "HOLLight.hollight.REAL_LT_TRANS"
obua@17644	964	"REAL_LT_TOTAL" > "HOLLight.hollight.REAL_LT_TOTAL"
obua@17644	965	"REAL_LT_SUB_RADD" > "HOLLight.hollight.REAL_LT_SUB_RADD"
obua@17644	966	"REAL_LT_SUB_LADD" > "HOLLight.hollight.REAL_LT_SUB_LADD"
kaliszyk@44639	967	"REAL_LT_SQUARE_ABS" > "HOLLight.hollight.REAL_LT_SQUARE_ABS"
obua@17644	968	"REAL_LT_SQUARE" > "HOLLight.hollight.REAL_LT_SQUARE"
obua@17644	969	"REAL_LT_RNEG" > "HOLLight.hollight.REAL_LT_RNEG"
obua@17644	970	"REAL_LT_RMUL_EQ" > "HOLLight.hollight.REAL_LT_RMUL_EQ"
obua@17644	971	"REAL_LT_RMUL" > "HOLLight.hollight.REAL_LT_RMUL"
kaliszyk@44639	972	"REAL_LT_RINV" > "HOLLight.hollight.REAL_LT_RINV"
obua@17644	973	"REAL_LT_REFL" > "HOLLight.hollight.REAL_LT_REFL"
obua@17644	974	"REAL_LT_RDIV_EQ" > "HOLLight.hollight.REAL_LT_RDIV_EQ"
obua@17644	975	"REAL_LT_RCANCEL_IMP" > "HOLLight.hollight.REAL_LT_RCANCEL_IMP"
obua@17644	976	"REAL_LT_RADD" > "HOLLight.hollight.REAL_LT_RADD"
obua@17644	977	"REAL_LT_POW2" > "HOLLight.hollight.REAL_LT_POW2"
obua@17644	978	"REAL_LT_NEGTOTAL" > "HOLLight.hollight.REAL_LT_NEGTOTAL"
obua@17644	979	"REAL_LT_NEG2" > "HOLLight.hollight.REAL_LT_NEG2"
obua@17644	980	"REAL_LT_NEG" > "HOLLight.hollight.REAL_LT_NEG"
kaliszyk@44639	981	"REAL_LT_MUL_EQ" > "HOLLight.hollight.REAL_LT_MUL_EQ"
obua@17644	982	"REAL_LT_MUL2" > "HOLLight.hollight.REAL_LT_MUL2"
obua@17644	983	"REAL_LT_MUL" > "HOLLight.hollight.REAL_LT_MUL"
obua@17644	984	"REAL_LT_MIN" > "HOLLight.hollight.REAL_LT_MIN"
obua@17644	985	"REAL_LT_MAX" > "HOLLight.hollight.REAL_LT_MAX"
obua@17644	986	"REAL_LT_LNEG" > "HOLLight.hollight.REAL_LT_LNEG"
obua@17644	987	"REAL_LT_LMUL_EQ" > "HOLLight.hollight.REAL_LT_LMUL_EQ"
obua@17644	988	"REAL_LT_LMUL" > "HOLLight.hollight.REAL_LT_LMUL"
kaliszyk@44639	989	"REAL_LT_LINV" > "HOLLight.hollight.REAL_LT_LINV"
obua@17644	990	"REAL_LT_LE" > "HOLLight.hollight.REAL_LT_LE"
obua@17644	991	"REAL_LT_LDIV_EQ" > "HOLLight.hollight.REAL_LT_LDIV_EQ"
obua@17644	992	"REAL_LT_LCANCEL_IMP" > "HOLLight.hollight.REAL_LT_LCANCEL_IMP"
obua@17644	993	"REAL_LT_LADD_IMP" > "HOLLight.hollight.REAL_LT_LADD_IMP"
obua@17644	994	"REAL_LT_LADD" > "HOLLight.hollight.REAL_LT_LADD"
obua@17644	995	"REAL_LT_INV_EQ" > "HOLLight.hollight.REAL_LT_INV_EQ"
obua@17644	996	"REAL_LT_INV2" > "HOLLight.hollight.REAL_LT_INV2"
obua@17644	997	"REAL_LT_INV" > "HOLLight.hollight.REAL_LT_INV"
obua@17644	998	"REAL_LT_IMP_NZ" > "HOLLight.hollight.REAL_LT_IMP_NZ"
obua@17644	999	"REAL_LT_IMP_NE" > "HOLLight.hollight.REAL_LT_IMP_NE"
obua@17644	1000	"REAL_LT_IMP_LE" > "HOLLight.hollight.REAL_LT_IMP_LE"
obua@17644	1001	"REAL_LT_GT" > "HOLLight.hollight.REAL_LT_GT"
obua@17644	1002	"REAL_LT_DIV2_EQ" > "HOLLight.hollight.REAL_LT_DIV2_EQ"
obua@17644	1003	"REAL_LT_DIV" > "HOLLight.hollight.REAL_LT_DIV"
obua@17644	1004	"REAL_LT_ANTISYM" > "HOLLight.hollight.REAL_LT_ANTISYM"
obua@17644	1005	"REAL_LT_ADD_SUB" > "HOLLight.hollight.REAL_LT_ADD_SUB"
obua@17644	1006	"REAL_LT_ADDR" > "HOLLight.hollight.REAL_LT_ADDR"
obua@17644	1007	"REAL_LT_ADDNEG2" > "HOLLight.hollight.REAL_LT_ADDNEG2"
obua@17644	1008	"REAL_LT_ADDNEG" > "HOLLight.hollight.REAL_LT_ADDNEG"
obua@17644	1009	"REAL_LT_ADDL" > "HOLLight.hollight.REAL_LT_ADDL"
obua@17644	1010	"REAL_LT_ADD2" > "HOLLight.hollight.REAL_LT_ADD2"
obua@17644	1011	"REAL_LT_ADD1" > "HOLLight.hollight.REAL_LT_ADD1"
obua@17644	1012	"REAL_LT_ADD" > "HOLLight.hollight.REAL_LT_ADD"
obua@17644	1013	"REAL_LT_01" > "HOLLight.hollight.REAL_LT_01"
obua@17644	1014	"REAL_LTE_TRANS" > "HOLLight.hollight.REAL_LTE_TRANS"
obua@17644	1015	"REAL_LTE_TOTAL" > "HOLLight.hollight.REAL_LTE_TOTAL"
obua@17644	1016	"REAL_LTE_ANTISYM" > "HOLLight.hollight.REAL_LTE_ANTISYM"
obua@17644	1017	"REAL_LTE_ADD2" > "HOLLight.hollight.REAL_LTE_ADD2"
obua@17644	1018	"REAL_LTE_ADD" > "HOLLight.hollight.REAL_LTE_ADD"
obua@17644	1019	"REAL_LNEG_UNIQ" > "HOLLight.hollight.REAL_LNEG_UNIQ"
obua@17644	1020	"REAL_LE_SUB_RADD" > "HOLLight.hollight.REAL_LE_SUB_RADD"
obua@17644	1021	"REAL_LE_SUB_LADD" > "HOLLight.hollight.REAL_LE_SUB_LADD"
obua@17644	1022	"REAL_LE_SQUARE_ABS" > "HOLLight.hollight.REAL_LE_SQUARE_ABS"
obua@17644	1023	"REAL_LE_SQUARE" > "HOLLight.hollight.REAL_LE_SQUARE"
obua@17644	1024	"REAL_LE_RNEG" > "HOLLight.hollight.REAL_LE_RNEG"
obua@17644	1025	"REAL_LE_RMUL_EQ" > "HOLLight.hollight.REAL_LE_RMUL_EQ"
obua@17644	1026	"REAL_LE_RMUL" > "HOLLight.hollight.REAL_LE_RMUL"
kaliszyk@44639	1027	"REAL_LE_RINV" > "HOLLight.hollight.REAL_LE_RINV"
obua@17644	1028	"REAL_LE_RDIV_EQ" > "HOLLight.hollight.REAL_LE_RDIV_EQ"
obua@17644	1029	"REAL_LE_RCANCEL_IMP" > "HOLLight.hollight.REAL_LE_RCANCEL_IMP"
obua@17644	1030	"REAL_LE_RADD" > "HOLLight.hollight.REAL_LE_RADD"
kaliszyk@44639	1031	"REAL_LE_POW_2" > "HOLLight.hollight.REAL_LE_POW_2"
obua@17644	1032	"REAL_LE_POW2" > "HOLLight.hollight.REAL_LE_POW2"
obua@17644	1033	"REAL_LE_NEGTOTAL" > "HOLLight.hollight.REAL_LE_NEGTOTAL"
obua@17644	1034	"REAL_LE_NEGR" > "HOLLight.hollight.REAL_LE_NEGR"
obua@17644	1035	"REAL_LE_NEGL" > "HOLLight.hollight.REAL_LE_NEGL"
obua@17644	1036	"REAL_LE_NEG2" > "HOLLight.hollight.REAL_LE_NEG2"
obua@17644	1037	"REAL_LE_NEG" > "HOLLight.hollight.REAL_LE_NEG"
kaliszyk@44639	1038	"REAL_LE_MUL_EQ" > "HOLLight.hollight.REAL_LE_MUL_EQ"
obua@17644	1039	"REAL_LE_MUL2" > "HOLLight.hollight.REAL_LE_MUL2"
obua@17644	1040	"REAL_LE_MIN" > "HOLLight.hollight.REAL_LE_MIN"
obua@17644	1041	"REAL_LE_MAX" > "HOLLight.hollight.REAL_LE_MAX"
obua@17644	1042	"REAL_LE_LT" > "HOLLight.hollight.REAL_LE_LT"
obua@17644	1043	"REAL_LE_LNEG" > "HOLLight.hollight.REAL_LE_LNEG"
obua@17644	1044	"REAL_LE_LMUL_EQ" > "HOLLight.hollight.REAL_LE_LMUL_EQ"
obua@17644	1045	"REAL_LE_LMUL" > "HOLLight.hollight.REAL_LE_LMUL"
kaliszyk@44639	1046	"REAL_LE_LINV" > "HOLLight.hollight.REAL_LE_LINV"
obua@17644	1047	"REAL_LE_LDIV_EQ" > "HOLLight.hollight.REAL_LE_LDIV_EQ"
obua@17644	1048	"REAL_LE_LCANCEL_IMP" > "HOLLight.hollight.REAL_LE_LCANCEL_IMP"
obua@17644	1049	"REAL_LE_LADD" > "HOLLight.hollight.REAL_LE_LADD"
obua@17644	1050	"REAL_LE_INV_EQ" > "HOLLight.hollight.REAL_LE_INV_EQ"
obua@17644	1051	"REAL_LE_INV2" > "HOLLight.hollight.REAL_LE_INV2"
obua@17644	1052	"REAL_LE_INV" > "HOLLight.hollight.REAL_LE_INV"
obua@17644	1053	"REAL_LE_DOUBLE" > "HOLLight.hollight.REAL_LE_DOUBLE"
obua@17644	1054	"REAL_LE_DIV2_EQ" > "HOLLight.hollight.REAL_LE_DIV2_EQ"
obua@17644	1055	"REAL_LE_DIV" > "HOLLight.hollight.REAL_LE_DIV"
obua@17644	1056	"REAL_LE_ADDR" > "HOLLight.hollight.REAL_LE_ADDR"
obua@17644	1057	"REAL_LE_ADDL" > "HOLLight.hollight.REAL_LE_ADDL"
obua@17644	1058	"REAL_LE_ADD2" > "HOLLight.hollight.REAL_LE_ADD2"
obua@17644	1059	"REAL_LE_ADD" > "HOLLight.hollight.REAL_LE_ADD"
obua@17644	1060	"REAL_LE_01" > "HOLLight.hollight.REAL_LE_01"
obua@17644	1061	"REAL_LET_TRANS" > "HOLLight.hollight.REAL_LET_TRANS"
obua@17644	1062	"REAL_LET_TOTAL" > "HOLLight.hollight.REAL_LET_TOTAL"
obua@17644	1063	"REAL_LET_ANTISYM" > "HOLLight.hollight.REAL_LET_ANTISYM"
obua@17644	1064	"REAL_LET_ADD2" > "HOLLight.hollight.REAL_LET_ADD2"
obua@17644	1065	"REAL_LET_ADD" > "HOLLight.hollight.REAL_LET_ADD"
kaliszyk@44639	1066	"REAL_INV_POW" > "HOLLight.hollight.REAL_INV_POW"
obua@17644	1067	"REAL_INV_NEG" > "HOLLight.hollight.REAL_INV_NEG"
obua@17644	1068	"REAL_INV_MUL" > "HOLLight.hollight.REAL_INV_MUL"
kaliszyk@44639	1069	"REAL_INV_LT_1" > "HOLLight.hollight.REAL_INV_LT_1"
obua@17644	1070	"REAL_INV_LE_1" > "HOLLight.hollight.REAL_INV_LE_1"
obua@17644	1071	"REAL_INV_INV" > "HOLLight.hollight.REAL_INV_INV"
kaliszyk@44639	1072	"REAL_INV_EQ_1" > "HOLLight.hollight.REAL_INV_EQ_1"
obua@17644	1073	"REAL_INV_EQ_0" > "HOLLight.hollight.REAL_INV_EQ_0"
obua@17644	1074	"REAL_INV_DIV" > "HOLLight.hollight.REAL_INV_DIV"
kaliszyk@44639	1075	"REAL_INV_1_LT" > "HOLLight.hollight.REAL_INV_1_LT"
obua@17644	1076	"REAL_INV_1_LE" > "HOLLight.hollight.REAL_INV_1_LE"
obua@17644	1077	"REAL_INV_1" > "HOLLight.hollight.REAL_INV_1"
kaliszyk@44639	1078	"REAL_INTEGRAL" > "HOLLight.hollight.REAL_INTEGRAL"
obua@17644	1079	"REAL_HREAL_LEMMA2" > "HOLLight.hollight.REAL_HREAL_LEMMA2"
obua@17644	1080	"REAL_HREAL_LEMMA1" > "HOLLight.hollight.REAL_HREAL_LEMMA1"
obua@17644	1081	"REAL_EQ_SUB_RADD" > "HOLLight.hollight.REAL_EQ_SUB_RADD"
obua@17644	1082	"REAL_EQ_SUB_LADD" > "HOLLight.hollight.REAL_EQ_SUB_LADD"
kaliszyk@44639	1083	"REAL_EQ_SQUARE_ABS" > "HOLLight.hollight.REAL_EQ_SQUARE_ABS"
obua@17644	1084	"REAL_EQ_RDIV_EQ" > "HOLLight.hollight.REAL_EQ_RDIV_EQ"
obua@17644	1085	"REAL_EQ_RCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_RCANCEL_IMP"
obua@17644	1086	"REAL_EQ_NEG2" > "HOLLight.hollight.REAL_EQ_NEG2"
obua@17644	1087	"REAL_EQ_MUL_RCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_RCANCEL"
obua@17644	1088	"REAL_EQ_MUL_LCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_LCANCEL"
obua@17644	1089	"REAL_EQ_LDIV_EQ" > "HOLLight.hollight.REAL_EQ_LDIV_EQ"
obua@17644	1090	"REAL_EQ_LCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_LCANCEL_IMP"
kaliszyk@44639	1091	"REAL_EQ_INV2" > "HOLLight.hollight.REAL_EQ_INV2"
obua@17644	1092	"REAL_EQ_IMP_LE" > "HOLLight.hollight.REAL_EQ_IMP_LE"
obua@17644	1093	"REAL_EQ_ADD_RCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL_0"
obua@17644	1094	"REAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL"
obua@17644	1095	"REAL_EQ_ADD_LCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL_0"
obua@17644	1096	"REAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL"
obua@17644	1097	"REAL_ENTIRE" > "HOLLight.hollight.REAL_ENTIRE"
obua@17644	1098	"REAL_DOWN2" > "HOLLight.hollight.REAL_DOWN2"
obua@17644	1099	"REAL_DOWN" > "HOLLight.hollight.REAL_DOWN"
obua@17644	1100	"REAL_DIV_RMUL" > "HOLLight.hollight.REAL_DIV_RMUL"
obua@17644	1101	"REAL_DIV_REFL" > "HOLLight.hollight.REAL_DIV_REFL"
obua@17644	1102	"REAL_DIV_POW2_ALT" > "HOLLight.hollight.REAL_DIV_POW2_ALT"
obua@17644	1103	"REAL_DIV_POW2" > "HOLLight.hollight.REAL_DIV_POW2"
obua@17644	1104	"REAL_DIV_LMUL" > "HOLLight.hollight.REAL_DIV_LMUL"
obua@17644	1105	"REAL_DIV_1" > "HOLLight.hollight.REAL_DIV_1"
obua@17644	1106	"REAL_DIFFSQ" > "HOLLight.hollight.REAL_DIFFSQ"
obua@17644	1107	"REAL_COMPLETE_SOMEPOS" > "HOLLight.hollight.REAL_COMPLETE_SOMEPOS"
obua@17644	1108	"REAL_COMPLETE" > "HOLLight.hollight.REAL_COMPLETE"
kaliszyk@44639	1109	"REAL_BOUNDS_LT" > "HOLLight.hollight.REAL_BOUNDS_LT"
kaliszyk@44639	1110	"REAL_BOUNDS_LE" > "HOLLight.hollight.REAL_BOUNDS_LE"
obua@17644	1111	"REAL_ADD_SUB2" > "HOLLight.hollight.REAL_ADD_SUB2"
obua@17644	1112	"REAL_ADD_SUB" > "HOLLight.hollight.REAL_ADD_SUB"
obua@17644	1113	"REAL_ADD_RINV" > "HOLLight.hollight.REAL_ADD_RINV"
obua@17644	1114	"REAL_ADD_RID" > "HOLLight.hollight.REAL_ADD_RID"
obua@17644	1115	"REAL_ADD_RDISTRIB" > "HOLLight.hollight.REAL_ADD_RDISTRIB"
obua@17644	1116	"REAL_ADD_AC" > "HOLLight.hollight.REAL_ADD_AC"
obua@17644	1117	"REAL_ADD2_SUB2" > "HOLLight.hollight.REAL_ADD2_SUB2"
obua@17644	1118	"REAL_ABS_ZERO" > "HOLLight.hollight.REAL_ABS_ZERO"
obua@17644	1119	"REAL_ABS_TRIANGLE_LT" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LT"
obua@17644	1120	"REAL_ABS_TRIANGLE_LE" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LE"
obua@17644	1121	"REAL_ABS_TRIANGLE" > "HOLLight.hollight.REAL_ABS_TRIANGLE"
obua@17644	1122	"REAL_ABS_SUB_ABS" > "HOLLight.hollight.REAL_ABS_SUB_ABS"
obua@17644	1123	"REAL_ABS_SUB" > "HOLLight.hollight.REAL_ABS_SUB"
obua@17644	1124	"REAL_ABS_STILLNZ" > "HOLLight.hollight.REAL_ABS_STILLNZ"
obua@17644	1125	"REAL_ABS_SIGN2" > "HOLLight.hollight.REAL_ABS_SIGN2"
obua@17644	1126	"REAL_ABS_SIGN" > "HOLLight.hollight.REAL_ABS_SIGN"
kaliszyk@44639	1127	"REAL_ABS_SGN" > "HOLLight.hollight.REAL_ABS_SGN"
obua@17644	1128	"REAL_ABS_REFL" > "HOLLight.hollight.REAL_ABS_REFL"
obua@17644	1129	"REAL_ABS_POW" > "HOLLight.hollight.REAL_ABS_POW"
obua@17644	1130	"REAL_ABS_POS" > "HOLLight.hollight.REAL_ABS_POS"
obua@17644	1131	"REAL_ABS_NZ" > "HOLLight.hollight.REAL_ABS_NZ"
obua@17644	1132	"REAL_ABS_NUM" > "HOLLight.hollight.REAL_ABS_NUM"
obua@17644	1133	"REAL_ABS_NEG" > "HOLLight.hollight.REAL_ABS_NEG"
obua@17644	1134	"REAL_ABS_MUL" > "HOLLight.hollight.REAL_ABS_MUL"
obua@17644	1135	"REAL_ABS_LE" > "HOLLight.hollight.REAL_ABS_LE"
obua@17644	1136	"REAL_ABS_INV" > "HOLLight.hollight.REAL_ABS_INV"
obua@17644	1137	"REAL_ABS_DIV" > "HOLLight.hollight.REAL_ABS_DIV"
obua@17644	1138	"REAL_ABS_CIRCLE" > "HOLLight.hollight.REAL_ABS_CIRCLE"
obua@17644	1139	"REAL_ABS_CASES" > "HOLLight.hollight.REAL_ABS_CASES"
obua@17644	1140	"REAL_ABS_BOUNDS" > "HOLLight.hollight.REAL_ABS_BOUNDS"
obua@17644	1141	"REAL_ABS_BOUND" > "HOLLight.hollight.REAL_ABS_BOUND"
obua@17644	1142	"REAL_ABS_BETWEEN2" > "HOLLight.hollight.REAL_ABS_BETWEEN2"
obua@17644	1143	"REAL_ABS_BETWEEN1" > "HOLLight.hollight.REAL_ABS_BETWEEN1"
obua@17644	1144	"REAL_ABS_BETWEEN" > "HOLLight.hollight.REAL_ABS_BETWEEN"
obua@17644	1145	"REAL_ABS_ABS" > "HOLLight.hollight.REAL_ABS_ABS"
obua@17644	1146	"REAL_ABS_1" > "HOLLight.hollight.REAL_ABS_1"
obua@17644	1147	"REAL_ABS_0" > "HOLLight.hollight.REAL_ABS_0"
obua@17644	1148	"RAT_LEMMA5" > "HOLLight.hollight.RAT_LEMMA5"
obua@17644	1149	"RAT_LEMMA4" > "HOLLight.hollight.RAT_LEMMA4"
obua@17644	1150	"RAT_LEMMA3" > "HOLLight.hollight.RAT_LEMMA3"
obua@17644	1151	"RAT_LEMMA2" > "HOLLight.hollight.RAT_LEMMA2"
obua@17644	1152	"RAT_LEMMA1" > "HOLLight.hollight.RAT_LEMMA1"
obua@17644	1153	"PSUBSET_UNIV" > "HOLLight.hollight.PSUBSET_UNIV"
kaliszyk@44639	1154	"PSUBSET_TRANS" > "Orderings.order_less_trans"
kaliszyk@44639	1155	"PSUBSET_SUBSET_TRANS" > "Orderings.order_less_le_trans"
obua@17644	1156	"PSUBSET_MEMBER" > "HOLLight.hollight.PSUBSET_MEMBER"
kaliszyk@44639	1157	"PSUBSET_IRREFL" > "Orderings.order_less_irrefl"
obua@17644	1158	"PSUBSET_INSERT_SUBSET" > "HOLLight.hollight.PSUBSET_INSERT_SUBSET"
kaliszyk@44639	1159	"PSUBSET_ALT" > "HOLLight.hollight.PSUBSET_ALT"
obua@17644	1160	"PRE_ELIM_THM" > "HOLLight.hollight.PRE_ELIM_THM"
kaliszyk@44639	1161	"POWERSET_CLAUSES" > "HOLLight.hollight.POWERSET_CLAUSES"
obua@17644	1162	"PASSOC_def" > "HOLLight.hollight.PASSOC_def"
kaliszyk@44639	1163	"PAIR_SURJECTIVE" > "Product_Type.prod.nchotomy"
obua@17644	1164	"PAIR_EXISTS_THM" > "HOLLight.hollight.PAIR_EXISTS_THM"
kaliszyk@44639	1165	"PAIR_EQ" > "Product_Type.Pair_eq"
obua@17644	1166	"PAIRWISE_def" > "HOLLight.hollight.PAIRWISE_def"
kaliszyk@44639	1167	"PAIRWISE_SING" > "HOLLight.hollight.PAIRWISE_SING"
kaliszyk@44639	1168	"PAIRWISE_MONO" > "HOLLight.hollight.PAIRWISE_MONO"
kaliszyk@44639	1169	"PAIRWISE_EMPTY" > "HOLLight.hollight.PAIRWISE_EMPTY"
kaliszyk@44639	1170	"PAIR" > "HOLLightCompat.PAIR"
obua@17644	1171	"OR_EXISTS_THM" > "HOL.ex_disj_distrib"
obua@17644	1172	"OR_CLAUSES" > "HOLLight.hollight.OR_CLAUSES"
kaliszyk@44639	1173	"ONE" > "Nat.One_nat_def"
kaliszyk@44639	1174	"ODD_SUB" > "HOLLight.hollight.ODD_SUB"
obua@17644	1175	"ODD_MULT" > "HOLLight.hollight.ODD_MULT"
obua@17644	1176	"ODD_MOD" > "HOLLight.hollight.ODD_MOD"
obua@17644	1177	"ODD_EXP" > "HOLLight.hollight.ODD_EXP"
kaliszyk@44639	1178	"ODD_EXISTS" > "Parity.odd_Suc_mult_two_ex"
obua@17644	1179	"ODD_DOUBLE" > "HOLLight.hollight.ODD_DOUBLE"
kaliszyk@44639	1180	"ODD_ADD" > "Parity.odd_add"
kaliszyk@44639	1181	"NUM_REP_def" > "HOLLight.hollight.NUM_REP_def"
kaliszyk@44639	1182	"NUM_OF_INT_OF_NUM" > "HOLLight.hollight.NUM_OF_INT_OF_NUM"
kaliszyk@44639	1183	"NUM_OF_INT" > "HOLLight.hollight.NUM_OF_INT"
obua@17644	1184	"NUM_INTEGRAL_LEMMA" > "HOLLight.hollight.NUM_INTEGRAL_LEMMA"
obua@17644	1185	"NUM_INTEGRAL" > "HOLLight.hollight.NUM_INTEGRAL"
kaliszyk@44639	1186	"NUM_GCD" > "HOLLight.hollight.NUM_GCD"
obua@17644	1187	"NUMSUM_def" > "HOLLight.hollight.NUMSUM_def"
obua@17644	1188	"NUMSUM_INJ" > "HOLLight.hollight.NUMSUM_INJ"
obua@17644	1189	"NUMSND_def" > "HOLLight.hollight.NUMSND_def"
kaliszyk@44639	1190	"NUMSEG_SING" > "SetInterval.order_class.atLeastAtMost_singleton"
obua@17644	1191	"NUMSEG_RREC" > "HOLLight.hollight.NUMSEG_RREC"
kaliszyk@44639	1192	"NUMSEG_REC" > "SetInterval.atLeastAtMostSuc_conv"
kaliszyk@44639	1193	"NUMSEG_OFFSET_IMAGE" > "SetInterval.image_add_atLeastAtMost"
kaliszyk@44639	1194	"NUMSEG_LT" > "HOLLight.hollight.NUMSEG_LT"
obua@17644	1195	"NUMSEG_LREC" > "HOLLight.hollight.NUMSEG_LREC"
kaliszyk@44639	1196	"NUMSEG_LE" > "HOLLight.hollight.NUMSEG_LE"
obua@17644	1197	"NUMSEG_EMPTY" > "HOLLight.hollight.NUMSEG_EMPTY"
obua@17644	1198	"NUMSEG_COMBINE_R" > "HOLLight.hollight.NUMSEG_COMBINE_R"
obua@17644	1199	"NUMSEG_COMBINE_L" > "HOLLight.hollight.NUMSEG_COMBINE_L"
obua@17644	1200	"NUMSEG_CLAUSES" > "HOLLight.hollight.NUMSEG_CLAUSES"
obua@17644	1201	"NUMSEG_ADD_SPLIT" > "HOLLight.hollight.NUMSEG_ADD_SPLIT"
obua@17644	1202	"NUMRIGHT_def" > "HOLLight.hollight.NUMRIGHT_def"
obua@17644	1203	"NUMPAIR_def" > "HOLLight.hollight.NUMPAIR_def"
obua@17644	1204	"NUMPAIR_INJ_LEMMA" > "HOLLight.hollight.NUMPAIR_INJ_LEMMA"
obua@17644	1205	"NUMPAIR_INJ" > "HOLLight.hollight.NUMPAIR_INJ"
obua@17644	1206	"NUMLEFT_def" > "HOLLight.hollight.NUMLEFT_def"
obua@17644	1207	"NUMFST_def" > "HOLLight.hollight.NUMFST_def"
obua@17644	1208	"NSUM_UNION_RZERO" > "HOLLight.hollight.NSUM_UNION_RZERO"
kaliszyk@44639	1209	"NSUM_UNION_NONZERO" > "HOLLight.hollight.NSUM_UNION_NONZERO"
obua@17644	1210	"NSUM_UNION_LZERO" > "HOLLight.hollight.NSUM_UNION_LZERO"
obua@17644	1211	"NSUM_UNION_EQ" > "HOLLight.hollight.NSUM_UNION_EQ"
kaliszyk@44639	1212	"NSUM_UNIONS_NONZERO" > "HOLLight.hollight.NSUM_UNIONS_NONZERO"
obua@17644	1213	"NSUM_UNION" > "HOLLight.hollight.NSUM_UNION"
obua@17644	1214	"NSUM_TRIV_NUMSEG" > "HOLLight.hollight.NSUM_TRIV_NUMSEG"
obua@17644	1215	"NSUM_SWAP_NUMSEG" > "HOLLight.hollight.NSUM_SWAP_NUMSEG"
obua@17644	1216	"NSUM_SWAP" > "HOLLight.hollight.NSUM_SWAP"
obua@17644	1217	"NSUM_SUPPORT" > "HOLLight.hollight.NSUM_SUPPORT"
obua@17644	1218	"NSUM_SUPERSET" > "HOLLight.hollight.NSUM_SUPERSET"
obua@17644	1219	"NSUM_SUBSET_SIMPLE" > "HOLLight.hollight.NSUM_SUBSET_SIMPLE"
obua@17644	1220	"NSUM_SUBSET" > "HOLLight.hollight.NSUM_SUBSET"
obua@17644	1221	"NSUM_SING_NUMSEG" > "HOLLight.hollight.NSUM_SING_NUMSEG"
obua@17644	1222	"NSUM_SING" > "HOLLight.hollight.NSUM_SING"
kaliszyk@44639	1223	"NSUM_RMUL" > "HOLLight.hollight.NSUM_RMUL"
obua@17644	1224	"NSUM_RESTRICT_SET" > "HOLLight.hollight.NSUM_RESTRICT_SET"
obua@17644	1225	"NSUM_RESTRICT" > "HOLLight.hollight.NSUM_RESTRICT"
obua@17644	1226	"NSUM_POS_BOUND" > "HOLLight.hollight.NSUM_POS_BOUND"
kaliszyk@44639	1227	"NSUM_PAIR" > "HOLLight.hollight.NSUM_PAIR"
obua@17644	1228	"NSUM_OFFSET_0" > "HOLLight.hollight.NSUM_OFFSET_0"
obua@17644	1229	"NSUM_OFFSET" > "HOLLight.hollight.NSUM_OFFSET"
obua@17644	1230	"NSUM_NSUM_RESTRICT" > "HOLLight.hollight.NSUM_NSUM_RESTRICT"
obua@19093	1231	"NSUM_NSUM_PRODUCT" > "HOLLight.hollight.NSUM_NSUM_PRODUCT"
obua@17644	1232	"NSUM_MULTICOUNT_GEN" > "HOLLight.hollight.NSUM_MULTICOUNT_GEN"
obua@17644	1233	"NSUM_MULTICOUNT" > "HOLLight.hollight.NSUM_MULTICOUNT"
obua@17644	1234	"NSUM_LT_ALL" > "HOLLight.hollight.NSUM_LT_ALL"
obua@17644	1235	"NSUM_LT" > "HOLLight.hollight.NSUM_LT"
kaliszyk@44639	1236	"NSUM_LMUL" > "HOLLight.hollight.NSUM_LMUL"
obua@17644	1237	"NSUM_LE_NUMSEG" > "HOLLight.hollight.NSUM_LE_NUMSEG"
obua@17644	1238	"NSUM_LE" > "HOLLight.hollight.NSUM_LE"
kaliszyk@44639	1239	"NSUM_INJECTION" > "HOLLight.hollight.NSUM_INJECTION"
kaliszyk@44639	1240	"NSUM_INCL_EXCL" > "HOLLight.hollight.NSUM_INCL_EXCL"
kaliszyk@44639	1241	"NSUM_IMAGE_NONZERO" > "HOLLight.hollight.NSUM_IMAGE_NONZERO"
obua@17644	1242	"NSUM_IMAGE_GEN" > "HOLLight.hollight.NSUM_IMAGE_GEN"
obua@17644	1243	"NSUM_IMAGE" > "HOLLight.hollight.NSUM_IMAGE"
kaliszyk@44639	1244	"NSUM_GROUP" > "HOLLight.hollight.NSUM_GROUP"
obua@17644	1245	"NSUM_EQ_SUPERSET" > "HOLLight.hollight.NSUM_EQ_SUPERSET"
obua@17644	1246	"NSUM_EQ_NUMSEG" > "HOLLight.hollight.NSUM_EQ_NUMSEG"
kaliszyk@44639	1247	"NSUM_EQ_GENERAL_INVERSES" > "HOLLight.hollight.NSUM_EQ_GENERAL_INVERSES"
obua@19093	1248	"NSUM_EQ_GENERAL" > "HOLLight.hollight.NSUM_EQ_GENERAL"
obua@17644	1249	"NSUM_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_NUMSEG"
kaliszyk@44639	1250	"NSUM_EQ_0_IFF_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_IFF_NUMSEG"
kaliszyk@44639	1251	"NSUM_EQ_0_IFF" > "HOLLight.hollight.NSUM_EQ_0_IFF"
obua@17644	1252	"NSUM_EQ_0" > "HOLLight.hollight.NSUM_EQ_0"
obua@17644	1253	"NSUM_EQ" > "HOLLight.hollight.NSUM_EQ"
obua@17644	1254	"NSUM_DIFF" > "HOLLight.hollight.NSUM_DIFF"
obua@17644	1255	"NSUM_DELTA" > "HOLLight.hollight.NSUM_DELTA"
kaliszyk@44639	1256	"NSUM_DELETE" > "HOLLight.hollight.NSUM_DELETE"
obua@17644	1257	"NSUM_CONST_NUMSEG" > "HOLLight.hollight.NSUM_CONST_NUMSEG"
obua@17644	1258	"NSUM_CONST" > "HOLLight.hollight.NSUM_CONST"
kaliszyk@44639	1259	"NSUM_CLOSED" > "HOLLight.hollight.NSUM_CLOSED"
obua@17644	1260	"NSUM_CLAUSES_RIGHT" > "HOLLight.hollight.NSUM_CLAUSES_RIGHT"
obua@17644	1261	"NSUM_CLAUSES_NUMSEG" > "HOLLight.hollight.NSUM_CLAUSES_NUMSEG"
obua@17644	1262	"NSUM_CLAUSES_LEFT" > "HOLLight.hollight.NSUM_CLAUSES_LEFT"
obua@17644	1263	"NSUM_CLAUSES" > "HOLLight.hollight.NSUM_CLAUSES"
kaliszyk@44639	1264	"NSUM_CASES" > "HOLLight.hollight.NSUM_CASES"
obua@17644	1265	"NSUM_BOUND_LT_GEN" > "HOLLight.hollight.NSUM_BOUND_LT_GEN"
obua@17644	1266	"NSUM_BOUND_LT_ALL" > "HOLLight.hollight.NSUM_BOUND_LT_ALL"
obua@17644	1267	"NSUM_BOUND_LT" > "HOLLight.hollight.NSUM_BOUND_LT"
obua@17644	1268	"NSUM_BOUND_GEN" > "HOLLight.hollight.NSUM_BOUND_GEN"
obua@17644	1269	"NSUM_BOUND" > "HOLLight.hollight.NSUM_BOUND"
obua@19093	1270	"NSUM_BIJECTION" > "HOLLight.hollight.NSUM_BIJECTION"
obua@17644	1271	"NSUM_ADD_SPLIT" > "HOLLight.hollight.NSUM_ADD_SPLIT"
obua@17644	1272	"NSUM_ADD_NUMSEG" > "HOLLight.hollight.NSUM_ADD_NUMSEG"
kaliszyk@44639	1273	"NSUM_ADD_GEN" > "HOLLight.hollight.NSUM_ADD_GEN"
obua@17644	1274	"NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
obua@17644	1275	"NSUM_0" > "HOLLight.hollight.NSUM_0"
kaliszyk@44789	1276	"NOT_UNIV_PSUBSET" > "Orderings.top_class.not_top_less"
kaliszyk@44639	1277	"NOT_SUC" > "Nat.Suc_not_Zero"
kaliszyk@44789	1278	"NOT_PSUBSET_EMPTY" > "Orderings.bot_class.not_less_bot"
obua@17644	1279	"NOT_ODD" > "HOLLight.hollight.NOT_ODD"
kaliszyk@44639	1280	"NOT_LT" > "Orderings.linorder_class.not_less"
kaliszyk@44639	1281	"NOT_LE" > "Orderings.linorder_class.not_le"
obua@17644	1282	"NOT_IN_EMPTY" > "HOLLight.hollight.NOT_IN_EMPTY"
kaliszyk@44639	1283	"NOT_INSERT_EMPTY" > "Set.insert_not_empty"
kaliszyk@44639	1284	"NOT_FORALL_THM" > "HOL.not_all"
kaliszyk@44639	1285	"NOT_EXISTS_THM" > "HOL.not_ex"
kaliszyk@44639	1286	"NOT_EX" > "HOLLightList.NOT_EX"
obua@17644	1287	"NOT_EVEN" > "HOLLight.hollight.NOT_EVEN"
obua@17644	1288	"NOT_EQUAL_SETS" > "HOLLight.hollight.NOT_EQUAL_SETS"
kaliszyk@44639	1289	"NOT_EMPTY_INSERT" > "Set.empty_not_insert"
kaliszyk@44639	1290	"NOT_CONS_NIL" > "List.list.distinct_2"
obua@17644	1291	"NOT_CLAUSES_WEAK" > "HOLLight.hollight.NOT_CLAUSES_WEAK"
kaliszyk@44639	1292	"NOT_ALL" > "HOLLightList.NOT_ALL"
obua@17644	1293	"NEUTRAL_REAL_MUL" > "HOLLight.hollight.NEUTRAL_REAL_MUL"
obua@17644	1294	"NEUTRAL_REAL_ADD" > "HOLLight.hollight.NEUTRAL_REAL_ADD"
obua@17644	1295	"NEUTRAL_MUL" > "HOLLight.hollight.NEUTRAL_MUL"
obua@17644	1296	"NEUTRAL_ADD" > "HOLLight.hollight.NEUTRAL_ADD"
obua@17644	1297	"NADD_UBOUND" > "HOLLight.hollight.NADD_UBOUND"
obua@17644	1298	"NADD_SUC" > "HOLLight.hollight.NADD_SUC"
obua@17644	1299	"NADD_RDISTRIB" > "HOLLight.hollight.NADD_RDISTRIB"
obua@17644	1300	"NADD_OF_NUM_WELLDEF" > "HOLLight.hollight.NADD_OF_NUM_WELLDEF"
obua@17644	1301	"NADD_OF_NUM_MUL" > "HOLLight.hollight.NADD_OF_NUM_MUL"
obua@17644	1302	"NADD_OF_NUM_LE" > "HOLLight.hollight.NADD_OF_NUM_LE"
obua@17644	1303	"NADD_OF_NUM_EQ" > "HOLLight.hollight.NADD_OF_NUM_EQ"
obua@17644	1304	"NADD_OF_NUM_ADD" > "HOLLight.hollight.NADD_OF_NUM_ADD"
obua@17644	1305	"NADD_OF_NUM" > "HOLLight.hollight.NADD_OF_NUM"
obua@17644	1306	"NADD_NONZERO" > "HOLLight.hollight.NADD_NONZERO"
obua@17644	1307	"NADD_MUL_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_MUL_WELLDEF_LEMMA"
obua@17644	1308	"NADD_MUL_WELLDEF" > "HOLLight.hollight.NADD_MUL_WELLDEF"
obua@17644	1309	"NADD_MUL_SYM" > "HOLLight.hollight.NADD_MUL_SYM"
obua@17644	1310	"NADD_MUL_LINV_LEMMA8" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA8"
obua@17644	1311	"NADD_MUL_LINV_LEMMA7a" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7a"
obua@17644	1312	"NADD_MUL_LINV_LEMMA7" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7"
obua@17644	1313	"NADD_MUL_LINV_LEMMA6" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA6"
obua@17644	1314	"NADD_MUL_LINV_LEMMA5" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA5"
obua@17644	1315	"NADD_MUL_LINV_LEMMA4" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA4"
obua@17644	1316	"NADD_MUL_LINV_LEMMA3" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA3"
obua@17644	1317	"NADD_MUL_LINV_LEMMA2" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA2"
obua@17644	1318	"NADD_MUL_LINV_LEMMA1" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA1"
obua@17644	1319	"NADD_MUL_LINV_LEMMA0" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA0"
obua@17644	1320	"NADD_MUL_LINV" > "HOLLight.hollight.NADD_MUL_LINV"
obua@17644	1321	"NADD_MUL_LID" > "HOLLight.hollight.NADD_MUL_LID"
obua@17644	1322	"NADD_MUL_ASSOC" > "HOLLight.hollight.NADD_MUL_ASSOC"
obua@17644	1323	"NADD_MULTIPLICATIVE" > "HOLLight.hollight.NADD_MULTIPLICATIVE"
obua@17644	1324	"NADD_MUL" > "HOLLight.hollight.NADD_MUL"
obua@17644	1325	"NADD_LE_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_LE_WELLDEF_LEMMA"
obua@17644	1326	"NADD_LE_WELLDEF" > "HOLLight.hollight.NADD_LE_WELLDEF"
obua@17644	1327	"NADD_LE_TRANS" > "HOLLight.hollight.NADD_LE_TRANS"
obua@17644	1328	"NADD_LE_TOTAL_LEMMA" > "HOLLight.hollight.NADD_LE_TOTAL_LEMMA"
obua@17644	1329	"NADD_LE_TOTAL" > "HOLLight.hollight.NADD_LE_TOTAL"
obua@17644	1330	"NADD_LE_RMUL" > "HOLLight.hollight.NADD_LE_RMUL"
obua@17644	1331	"NADD_LE_REFL" > "HOLLight.hollight.NADD_LE_REFL"
obua@17644	1332	"NADD_LE_RADD" > "HOLLight.hollight.NADD_LE_RADD"
obua@17644	1333	"NADD_LE_LMUL" > "HOLLight.hollight.NADD_LE_LMUL"
obua@17644	1334	"NADD_LE_LADD" > "HOLLight.hollight.NADD_LE_LADD"
obua@17644	1335	"NADD_LE_EXISTS" > "HOLLight.hollight.NADD_LE_EXISTS"
obua@17644	1336	"NADD_LE_ANTISYM" > "HOLLight.hollight.NADD_LE_ANTISYM"
obua@17644	1337	"NADD_LE_ADD" > "HOLLight.hollight.NADD_LE_ADD"
obua@17644	1338	"NADD_LE_0" > "HOLLight.hollight.NADD_LE_0"
obua@17644	1339	"NADD_LDISTRIB" > "HOLLight.hollight.NADD_LDISTRIB"
obua@17644	1340	"NADD_LBOUND" > "HOLLight.hollight.NADD_LBOUND"
obua@17644	1341	"NADD_INV_WELLDEF" > "HOLLight.hollight.NADD_INV_WELLDEF"
obua@17644	1342	"NADD_INV_0" > "HOLLight.hollight.NADD_INV_0"
obua@17644	1343	"NADD_INV" > "HOLLight.hollight.NADD_INV"
obua@17644	1344	"NADD_EQ_TRANS" > "HOLLight.hollight.NADD_EQ_TRANS"
obua@17644	1345	"NADD_EQ_SYM" > "HOLLight.hollight.NADD_EQ_SYM"
obua@17644	1346	"NADD_EQ_REFL" > "HOLLight.hollight.NADD_EQ_REFL"
obua@17644	1347	"NADD_EQ_IMP_LE" > "HOLLight.hollight.NADD_EQ_IMP_LE"
obua@17644	1348	"NADD_DIST_LEMMA" > "HOLLight.hollight.NADD_DIST_LEMMA"
obua@17644	1349	"NADD_DIST" > "HOLLight.hollight.NADD_DIST"
obua@17644	1350	"NADD_COMPLETE" > "HOLLight.hollight.NADD_COMPLETE"
obua@17644	1351	"NADD_CAUCHY" > "HOLLight.hollight.NADD_CAUCHY"
obua@17644	1352	"NADD_BOUND" > "HOLLight.hollight.NADD_BOUND"
obua@17644	1353	"NADD_ARCH_ZERO" > "HOLLight.hollight.NADD_ARCH_ZERO"
obua@17644	1354	"NADD_ARCH_MULT" > "HOLLight.hollight.NADD_ARCH_MULT"
obua@17644	1355	"NADD_ARCH_LEMMA" > "HOLLight.hollight.NADD_ARCH_LEMMA"
obua@17644	1356	"NADD_ARCH" > "HOLLight.hollight.NADD_ARCH"
obua@17644	1357	"NADD_ALTMUL" > "HOLLight.hollight.NADD_ALTMUL"
obua@17644	1358	"NADD_ADD_WELLDEF" > "HOLLight.hollight.NADD_ADD_WELLDEF"
obua@17644	1359	"NADD_ADD_SYM" > "HOLLight.hollight.NADD_ADD_SYM"
obua@17644	1360	"NADD_ADD_LID" > "HOLLight.hollight.NADD_ADD_LID"
obua@17644	1361	"NADD_ADD_LCANCEL" > "HOLLight.hollight.NADD_ADD_LCANCEL"
obua@17644	1362	"NADD_ADD_ASSOC" > "HOLLight.hollight.NADD_ADD_ASSOC"
obua@17644	1363	"NADD_ADDITIVE" > "HOLLight.hollight.NADD_ADDITIVE"
obua@17644	1364	"NADD_ADD" > "HOLLight.hollight.NADD_ADD"
kaliszyk@44639	1365	"MULT_SYM" > "Fields.linordered_field_class.sign_simps_40"
obua@17644	1366	"MULT_SUC" > "Nat.mult_Suc_right"
kaliszyk@44639	1367	"MULT_EXP" > "Power.comm_monoid_mult_class.power_mult_distrib"
kaliszyk@44639	1368	"MULT_EQ_1" > "Nat.nat_mult_eq_1_iff"
obua@17644	1369	"MULT_EQ_0" > "Nat.mult_is_0"
kaliszyk@44639	1370	"MULT_DIV_LE" > "HOLLight.hollight.MULT_DIV_LE"
obua@17644	1371	"MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
kaliszyk@44639	1372	"MULT_ASSOC" > "Fields.linordered_field_class.sign_simps_41"
obua@17644	1373	"MULT_AC" > "HOLLight.hollight.MULT_AC"
kaliszyk@44639	1374	"MULT_2" > "Int.semiring_mult_2"
kaliszyk@44639	1375	"MULT_0" > "Divides.arithmetic_simps_41"
obua@17644	1376	"MONO_FORALL" > "Inductive.basic_monos_6"
obua@17644	1377	"MONO_EXISTS" > "Inductive.basic_monos_5"
obua@17644	1378	"MONO_COND" > "HOLLight.hollight.MONO_COND"
kaliszyk@44639	1379	"MONO_ALL2" > "List.list_all2_mono"
kaliszyk@44639	1380	"MONO_ALL" > "HOLLightList.MONO_ALL"
obua@17644	1381	"MONOIDAL_REAL_MUL" > "HOLLight.hollight.MONOIDAL_REAL_MUL"
obua@17644	1382	"MONOIDAL_REAL_ADD" > "HOLLight.hollight.MONOIDAL_REAL_ADD"
obua@17644	1383	"MONOIDAL_MUL" > "HOLLight.hollight.MONOIDAL_MUL"
obua@17644	1384	"MONOIDAL_ADD" > "HOLLight.hollight.MONOIDAL_ADD"
kaliszyk@44639	1385	"MONOIDAL_AC" > "HOLLight.hollight.MONOIDAL_AC"
obua@17644	1386	"MOD_UNIQ" > "HOLLight.hollight.MOD_UNIQ"
obua@17644	1387	"MOD_MULT_RMOD" > "HOLLight.hollight.MOD_MULT_RMOD"
obua@17644	1388	"MOD_MULT_MOD2" > "HOLLight.hollight.MOD_MULT_MOD2"
obua@17644	1389	"MOD_MULT_LMOD" > "HOLLight.hollight.MOD_MULT_LMOD"
kaliszyk@44639	1390	"MOD_MULT_ADD" > "Divides.mod_mult_self3"
obua@17644	1391	"MOD_MULT2" > "HOLLight.hollight.MOD_MULT2"
obua@17644	1392	"MOD_MOD_REFL" > "HOLLight.hollight.MOD_MOD_REFL"
obua@17644	1393	"MOD_MOD" > "HOLLight.hollight.MOD_MOD"
kaliszyk@44639	1394	"MOD_LT" > "Divides.mod_less"
obua@17644	1395	"MOD_LE" > "HOLLight.hollight.MOD_LE"
obua@17644	1396	"MOD_EXP_MOD" > "HOLLight.hollight.MOD_EXP_MOD"
obua@17644	1397	"MOD_EXISTS" > "HOLLight.hollight.MOD_EXISTS"
obua@17644	1398	"MOD_EQ_0" > "HOLLight.hollight.MOD_EQ_0"
obua@17644	1399	"MOD_EQ" > "HOLLight.hollight.MOD_EQ"
obua@17644	1400	"MOD_ADD_MOD" > "HOLLight.hollight.MOD_ADD_MOD"
obua@17644	1401	"MK_REC_INJ" > "HOLLight.hollight.MK_REC_INJ"
obua@17644	1402	"MINIMAL" > "HOLLight.hollight.MINIMAL"
kaliszyk@44639	1403	"MEM_MAP" > "HOLLightList.MEM_MAP"
kaliszyk@44639	1404	"MEM_FILTER" > "HOLLightList.MEM_FILTER"
kaliszyk@44639	1405	"MEM_EXISTS_EL" > "HOLLightList.MEM_EXISTS_EL"
kaliszyk@44639	1406	"MEM_EL" > "List.nth_mem"
kaliszyk@44639	1407	"MEM_APPEND" > "HOLLightList.MEM_APPEND"
kaliszyk@44639	1408	"MEMBER_NOT_EMPTY" > "Set.ex_in_conv"
obua@17644	1409	"MEASURE_LE" > "HOLLight.hollight.MEASURE_LE"
kaliszyk@44639	1410	"MATCH_SEQPATTERN" > "HOLLight.hollight.MATCH_SEQPATTERN"
kaliszyk@44639	1411	"MAP_o" > "List.map.compositionality"
kaliszyk@44639	1412	"MAP_SND_ZIP" > "List.map_snd_zip"
kaliszyk@44639	1413	"MAP_ID" > "List.map_ident"
kaliszyk@44639	1414	"MAP_I" > "List.map.id"
kaliszyk@44639	1415	"MAP_FST_ZIP" > "List.map_fst_zip"
kaliszyk@44639	1416	"MAP_EQ_NIL" > "List.map_is_Nil_conv"
kaliszyk@44639	1417	"MAP_EQ_DEGEN" > "HOLLightList.MAP_EQ_DEGEN"
kaliszyk@44639	1418	"MAP_EQ_ALL2" > "HOLLightList.MAP_EQ_ALL2"
kaliszyk@44639	1419	"MAP_EQ" > "HOLLightList.MAP_EQ"
kaliszyk@44639	1420	"MAP_APPEND" > "List.map_append"
kaliszyk@44639	1421	"MAP2" > "HOLLightList.MAP2"
kaliszyk@44639	1422	"LT_TRANS" > "Orderings.order_less_trans"
kaliszyk@44639	1423	"LT_SUC_LE" > "Nat.le_simps_2"
kaliszyk@44639	1424	"LT_SUC" > "Nat.Suc_less_eq"
kaliszyk@44639	1425	"LT_REFL" > "Nat.less_not_refl"
kaliszyk@44639	1426	"LT_NZ" > "Nat.neq0_conv"
obua@17644	1427	"LT_MULT_RCANCEL" > "HOLLight.hollight.LT_MULT_RCANCEL"
obua@17644	1428	"LT_MULT_LCANCEL" > "HOLLight.hollight.LT_MULT_LCANCEL"
obua@17644	1429	"LT_MULT2" > "HOLLight.hollight.LT_MULT2"
kaliszyk@44639	1430	"LT_MULT" > "Nat.nat_0_less_mult_iff"
obua@17644	1431	"LT_LMULT" > "HOLLight.hollight.LT_LMULT"
kaliszyk@44639	1432	"LT_LE" > "Nat.nat_less_le"
kaliszyk@44639	1433	"LT_IMP_LE" > "FunDef.termination_basic_simps_5"
obua@17644	1434	"LT_EXP" > "HOLLight.hollight.LT_EXP"
obua@17644	1435	"LT_EXISTS" > "HOLLight.hollight.LT_EXISTS"
obua@17644	1436	"LT_CASES" > "HOLLight.hollight.LT_CASES"
obua@17644	1437	"LT_ANTISYM" > "HOLLight.hollight.LT_ANTISYM"
kaliszyk@44639	1438	"LT_ADD_RCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_right"
kaliszyk@44639	1439	"LT_ADD_LCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_left"
obua@17644	1440	"LT_ADDR" > "HOLLight.hollight.LT_ADDR"
kaliszyk@44639	1441	"LT_ADD2" > "Groups.add_mono_thms_linordered_field_5"
obua@17644	1442	"LT_ADD" > "HOLLight.hollight.LT_ADD"
kaliszyk@44639	1443	"LT_0" > "Nat.zero_less_Suc"
kaliszyk@44639	1444	"LTE_TRANS" > "Orderings.order_less_le_trans"
obua@17644	1445	"LTE_CASES" > "HOLLight.hollight.LTE_CASES"
obua@17644	1446	"LTE_ANTISYM" > "HOLLight.hollight.LTE_ANTISYM"
kaliszyk@44639	1447	"LTE_ADD2" > "Groups.add_mono_thms_linordered_field_3"
kaliszyk@44639	1448	"LE_TRANS" > "Nat.le_trans"
kaliszyk@44639	1449	"LE_SUC_LT" > "Nat.Suc_le_eq"
kaliszyk@44639	1450	"LE_SUC" > "Nat.Suc_le_mono"
kaliszyk@44639	1451	"LE_SQUARE_REFL" > "Nat.le_square"
kaliszyk@44639	1452	"LE_REFL" > "Nat.le_refl"
obua@17644	1453	"LE_RDIV_EQ" > "HOLLight.hollight.LE_RDIV_EQ"
obua@17644	1454	"LE_MULT_RCANCEL" > "HOLLight.hollight.LE_MULT_RCANCEL"
obua@17644	1455	"LE_MULT_LCANCEL" > "HOLLight.hollight.LE_MULT_LCANCEL"
kaliszyk@44639	1456	"LE_MULT2" > "Nat.mult_le_mono"
kaliszyk@44639	1457	"LE_LT" > "Nat.le_eq_less_or_eq"
obua@17644	1458	"LE_LDIV_EQ" > "HOLLight.hollight.LE_LDIV_EQ"
obua@17644	1459	"LE_LDIV" > "HOLLight.hollight.LE_LDIV"
obua@17644	1460	"LE_EXP" > "HOLLight.hollight.LE_EXP"
kaliszyk@44639	1461	"LE_EXISTS" > "Nat.le_iff_add"
kaliszyk@44639	1462	"LE_CASES" > "Nat.nat_le_linear"
kaliszyk@44639	1463	"LE_C" > "HOLLight.hollight.LE_C"
kaliszyk@44639	1464	"LE_ANTISYM" > "Orderings.order_class.eq_iff"
kaliszyk@44639	1465	"LE_ADD_RCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_right"
kaliszyk@44639	1466	"LE_ADD_LCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left"
kaliszyk@44639	1467	"LE_ADDR" > "Nat.le_add2"
kaliszyk@44639	1468	"LE_ADD2" > "Groups.add_mono_thms_linordered_semiring_1"
kaliszyk@44639	1469	"LE_ADD" > "Nat.le_add1"
kaliszyk@44639	1470	"LE_1" > "HOLLight.hollight.LE_1"
kaliszyk@44639	1471	"LE_0" > "Nat.le0"
kaliszyk@44639	1472	"LET_TRANS" > "Orderings.order_le_less_trans"
obua@17644	1473	"LET_END_def" > "HOLLight.hollight.LET_END_def"
kaliszyk@44639	1474	"LET_CASES" > "Orderings.linorder_class.le_less_linear"
obua@17644	1475	"LET_ANTISYM" > "HOLLight.hollight.LET_ANTISYM"
kaliszyk@44639	1476	"LET_ADD2" > "Groups.add_mono_thms_linordered_field_4"
kaliszyk@44639	1477	"LENGTH_TL" > "HOLLightList.LENGTH_TL"
kaliszyk@44639	1478	"LENGTH_REPLICATE" > "List.length_replicate"
kaliszyk@44639	1479	"LENGTH_MAP2" > "HOLLightList.LENGTH_MAP2"
kaliszyk@44639	1480	"LENGTH_MAP" > "List.length_map"
kaliszyk@44639	1481	"LENGTH_EQ_NIL" > "List.length_0_conv"
kaliszyk@44639	1482	"LENGTH_EQ_CONS" > "List.length_Suc_conv"
kaliszyk@44639	1483	"LENGTH_APPEND" > "List.length_append"
kaliszyk@44639	1484	"LEFT_SUB_DISTRIB" > "Nat.diff_mult_distrib2"
obua@17644	1485	"LEFT_OR_FORALL_THM" > "HOL.all_simps_3"
obua@17644	1486	"LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
kaliszyk@44639	1487	"LEFT_OR_DISTRIB" > "Groebner_Basis.dnf_1"
kaliszyk@44639	1488	"LEFT_IMP_FORALL_THM" > "HOL.ex_simps_5"
kaliszyk@44639	1489	"LEFT_IMP_EXISTS_THM" > "HOL.all_simps_5"
obua@17644	1490	"LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
kaliszyk@44639	1491	"LEFT_FORALL_IMP_THM" > "HOL.all_simps_5"
kaliszyk@44639	1492	"LEFT_EXISTS_IMP_THM" > "HOL.ex_simps_5"
obua@17644	1493	"LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
obua@17644	1494	"LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
obua@17644	1495	"LEFT_AND_EXISTS_THM" > "HOL.ex_simps_1"
kaliszyk@44639	1496	"LEFT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_25"
kaliszyk@44639	1497	"LAST_EL" > "List.last_conv_nth"
kaliszyk@44639	1498	"LAST_CLAUSES" > "HOLLightList.LAST_CLAUSES"
kaliszyk@44639	1499	"LAST_APPEND" > "List.last_append"
obua@17644	1500	"LAMBDA_UNIQUE" > "HOLLight.hollight.LAMBDA_UNIQUE"
kaliszyk@44639	1501	"LAMBDA_PAIR_THM" > "HOLLight.hollight.LAMBDA_PAIR_THM"
obua@17644	1502	"LAMBDA_ETA" > "HOLLight.hollight.LAMBDA_ETA"
obua@17644	1503	"LAMBDA_BETA" > "HOLLight.hollight.LAMBDA_BETA"
kaliszyk@44639	1504	"I_THM" > "HOL.refl"
obua@17644	1505	"I_O_ID" > "HOLLight.hollight.I_O_ID"
obua@17644	1506	"ITSET_def" > "HOLLight.hollight.ITSET_def"
obua@17644	1507	"ITSET_EQ" > "HOLLight.hollight.ITSET_EQ"
kaliszyk@44639	1508	"ITLIST_EXTRA" > "HOLLightList.ITLIST_EXTRA"
kaliszyk@44639	1509	"ITLIST_APPEND" > "List.foldr_append"
kaliszyk@44639	1510	"ITLIST2" > "HOLLightList.ITLIST2"
kaliszyk@44639	1511	"ITERATE_UNION_NONZERO" > "HOLLight.hollight.ITERATE_UNION_NONZERO"
obua@17644	1512	"ITERATE_UNION_GEN" > "HOLLight.hollight.ITERATE_UNION_GEN"
obua@17644	1513	"ITERATE_UNION" > "HOLLight.hollight.ITERATE_UNION"
obua@17644	1514	"ITERATE_SUPPORT" > "HOLLight.hollight.ITERATE_SUPPORT"
kaliszyk@44639	1515	"ITERATE_SUPERSET" > "HOLLight.hollight.ITERATE_SUPERSET"
obua@17644	1516	"ITERATE_SING" > "HOLLight.hollight.ITERATE_SING"
obua@17644	1517	"ITERATE_RELATED" > "HOLLight.hollight.ITERATE_RELATED"
kaliszyk@44639	1518	"ITERATE_PAIR" > "HOLLight.hollight.ITERATE_PAIR"
kaliszyk@44639	1519	"ITERATE_OP_GEN" > "HOLLight.hollight.ITERATE_OP_GEN"
kaliszyk@44639	1520	"ITERATE_OP" > "HOLLight.hollight.ITERATE_OP"
obua@19093	1521	"ITERATE_ITERATE_PRODUCT" > "HOLLight.hollight.ITERATE_ITERATE_PRODUCT"
kaliszyk@44639	1522	"ITERATE_INJECTION" > "HOLLight.hollight.ITERATE_INJECTION"
kaliszyk@44639	1523	"ITERATE_INCL_EXCL" > "HOLLight.hollight.ITERATE_INCL_EXCL"
kaliszyk@44639	1524	"ITERATE_IMAGE_NONZERO" > "HOLLight.hollight.ITERATE_IMAGE_NONZERO"
obua@17644	1525	"ITERATE_IMAGE" > "HOLLight.hollight.ITERATE_IMAGE"
kaliszyk@44639	1526	"ITERATE_EXPAND_CASES" > "HOLLight.hollight.ITERATE_EXPAND_CASES"
obua@17644	1527	"ITERATE_EQ_NEUTRAL" > "HOLLight.hollight.ITERATE_EQ_NEUTRAL"
kaliszyk@44639	1528	"ITERATE_EQ_GENERAL_INVERSES" > "HOLLight.hollight.ITERATE_EQ_GENERAL_INVERSES"
obua@19093	1529	"ITERATE_EQ_GENERAL" > "HOLLight.hollight.ITERATE_EQ_GENERAL"
obua@19093	1530	"ITERATE_EQ" > "HOLLight.hollight.ITERATE_EQ"
obua@17644	1531	"ITERATE_DIFF_GEN" > "HOLLight.hollight.ITERATE_DIFF_GEN"
obua@17644	1532	"ITERATE_DIFF" > "HOLLight.hollight.ITERATE_DIFF"
obua@17644	1533	"ITERATE_DELTA" > "HOLLight.hollight.ITERATE_DELTA"
kaliszyk@44639	1534	"ITERATE_DELETE" > "HOLLight.hollight.ITERATE_DELETE"
obua@17644	1535	"ITERATE_CLOSED" > "HOLLight.hollight.ITERATE_CLOSED"
kaliszyk@44639	1536	"ITERATE_CLAUSES_NUMSEG" > "HOLLight.hollight.ITERATE_CLAUSES_NUMSEG"
obua@17644	1537	"ITERATE_CLAUSES_GEN" > "HOLLight.hollight.ITERATE_CLAUSES_GEN"
obua@17644	1538	"ITERATE_CLAUSES" > "HOLLight.hollight.ITERATE_CLAUSES"
kaliszyk@44639	1539	"ITERATE_CASES" > "HOLLight.hollight.ITERATE_CASES"
obua@19093	1540	"ITERATE_BIJECTION" > "HOLLight.hollight.ITERATE_BIJECTION"
obua@17644	1541	"ISO_def" > "HOLLight.hollight.ISO_def"
obua@17644	1542	"ISO_USAGE" > "HOLLight.hollight.ISO_USAGE"
obua@17644	1543	"ISO_REFL" > "HOLLight.hollight.ISO_REFL"
obua@17644	1544	"ISO_FUN" > "HOLLight.hollight.ISO_FUN"
kaliszyk@44639	1545	"IN_UNIV" > "Set.UNIV_I"
obua@17644	1546	"IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
kaliszyk@44639	1547	"IN_UNION" > "Complete_Lattice.mem_simps_3"
obua@17644	1548	"IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
kaliszyk@44639	1549	"IN_SING" > "Set.singleton_iff"
kaliszyk@44714	1550	"IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
obua@17644	1551	"IN_REST" > "HOLLight.hollight.IN_REST"
kaliszyk@44639	1552	"IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
kaliszyk@44639	1553	"IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
obua@17644	1554	"IN_INTERS" > "HOLLight.hollight.IN_INTERS"
kaliszyk@44639	1555	"IN_INTER" > "Complete_Lattice.mem_simps_4"
kaliszyk@44639	1556	"IN_INSERT" > "Complete_Lattice.mem_simps_1"
obua@17644	1557	"IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
obua@17644	1558	"IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
obua@19093	1559	"IN_ELIM_PAIR_THM" > "HOLLight.hollight.IN_ELIM_PAIR_THM"
obua@17644	1560	"IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
kaliszyk@44639	1561	"IN_DIFF" > "Complete_Lattice.mem_simps_6"
obua@17644	1562	"IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
obua@17644	1563	"IN_DELETE" > "HOLLight.hollight.IN_DELETE"
kaliszyk@44639	1564	"IN_CROSS" > "HOLLight.hollight.IN_CROSS"
kaliszyk@44639	1565	"INT_WOP" > "HOLLight.hollight.INT_WOP"
obua@17644	1566	"INT_POW" > "HOLLight.hollight.INT_POW"
kaliszyk@44639	1567	"INT_OF_NUM_OF_INT" > "HOLLight.hollight.INT_OF_NUM_OF_INT"
obua@17644	1568	"INT_LT_DISCRETE" > "HOLLight.hollight.INT_LT_DISCRETE"
obua@17644	1569	"INT_LT" > "HOLLight.hollight.INT_LT"
kaliszyk@44639	1570	"INT_INTEGRAL" > "HOLLight.hollight.INT_INTEGRAL"
obua@17644	1571	"INT_IMAGE" > "HOLLight.hollight.INT_IMAGE"
obua@17644	1572	"INT_GT_DISCRETE" > "HOLLight.hollight.INT_GT_DISCRETE"
obua@17644	1573	"INT_GT" > "HOLLight.hollight.INT_GT"
obua@17644	1574	"INT_GE" > "HOLLight.hollight.INT_GE"
kaliszyk@44639	1575	"INT_GCD_EXISTS_POS" > "HOLLight.hollight.INT_GCD_EXISTS_POS"
kaliszyk@44639	1576	"INT_GCD_EXISTS" > "HOLLight.hollight.INT_GCD_EXISTS"
obua@17644	1577	"INT_FORALL_POS" > "HOLLight.hollight.INT_FORALL_POS"
kaliszyk@44639	1578	"INT_FORALL_ABS" > "HOLLight.hollight.INT_FORALL_ABS"
kaliszyk@44639	1579	"INT_EXISTS_POS" > "HOLLight.hollight.INT_EXISTS_POS"
kaliszyk@44639	1580	"INT_EXISTS_ABS" > "HOLLight.hollight.INT_EXISTS_ABS"
kaliszyk@44639	1581	"INT_DIVMOD_UNIQ" > "HOLLight.hollight.INT_DIVMOD_UNIQ"
kaliszyk@44639	1582	"INT_DIVMOD_EXIST_0" > "HOLLight.hollight.INT_DIVMOD_EXIST_0"
kaliszyk@44639	1583	"INT_DIVISION" > "HOLLight.hollight.INT_DIVISION"
obua@17644	1584	"INT_ARCH" > "HOLLight.hollight.INT_ARCH"
obua@17644	1585	"INT_ABS_MUL_1" > "HOLLight.hollight.INT_ABS_MUL_1"
obua@17644	1586	"INT_ABS" > "HOLLight.hollight.INT_ABS"
obua@17644	1587	"INTER_UNIV" > "HOLLight.hollight.INTER_UNIV"
kaliszyk@44639	1588	"INTER_UNIONS" > "HOLLight.hollight.INTER_UNIONS"
obua@17644	1589	"INTER_SUBSET" > "HOLLight.hollight.INTER_SUBSET"
kaliszyk@44639	1590	"INTER_OVER_UNION" > "Lattices.distrib_lattice_class.distrib_1"
kaliszyk@44639	1591	"INTER_IDEMPOT" > "Big_Operators.lattice_class.Inf_fin.idem"
obua@17644	1592	"INTER_EMPTY" > "HOLLight.hollight.INTER_EMPTY"
kaliszyk@44639	1593	"INTER_COMM" > "Lattices.lattice_class.inf_sup_aci_1"
kaliszyk@44639	1594	"INTER_ASSOC" > "Lattices.lattice_class.inf_sup_aci_2"
obua@17644	1595	"INTER_ACI" > "HOLLight.hollight.INTER_ACI"
kaliszyk@44639	1596	"INTERS_UNIONS" > "HOLLight.hollight.INTERS_UNIONS"
kaliszyk@44639	1597	"INTERS_INSERT" > "Complete_Lattice.Inter_insert"
kaliszyk@44639	1598	"INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
kaliszyk@44639	1599	"INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
kaliszyk@44639	1600	"INTERS_2" > "Complete_Lattice.Int_eq_Inter"
kaliszyk@44639	1601	"INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
kaliszyk@44639	1602	"INTERS_0" > "Complete_Lattice.Inter_empty"
obua@17644	1603	"INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
kaliszyk@44639	1604	"INSERT_UNION_EQ" > "Set.Un_insert_left"
obua@17644	1605	"INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
kaliszyk@44639	1606	"INSERT_SUBSET" > "Set.insert_subset"
kaliszyk@44639	1607	"INSERT_INTER" > "Set.Int_insert_left"
kaliszyk@44639	1608	"INSERT_INSERT" > "Set.insert_absorb2"
kaliszyk@44639	1609	"INSERT_DIFF" > "Set.insert_Diff_if"
kaliszyk@44639	1610	"INSERT_DELETE" > "Set.insert_Diff"
kaliszyk@44639	1611	"INSERT_COMM" > "Set.insert_commute"
obua@17644	1612	"INSERT_AC" > "HOLLight.hollight.INSERT_AC"
obua@17644	1613	"INSERT" > "HOLLight.hollight.INSERT"
obua@17644	1614	"INJ_def" > "HOLLight.hollight.INJ_def"
obua@17644	1615	"INJ_INVERSE2" > "HOLLight.hollight.INJ_INVERSE2"
obua@17644	1616	"INJP_def" > "HOLLight.hollight.INJP_def"
obua@17644	1617	"INJP_INJ" > "HOLLight.hollight.INJP_INJ"
obua@17644	1618	"INJN_def" > "HOLLight.hollight.INJN_def"
obua@17644	1619	"INJN_INJ" > "HOLLight.hollight.INJN_INJ"
obua@17644	1620	"INJF_def" > "HOLLight.hollight.INJF_def"
obua@17644	1621	"INJF_INJ" > "HOLLight.hollight.INJF_INJ"
obua@17644	1622	"INJECTIVE_ON_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_ON_LEFT_INVERSE"
kaliszyk@44639	1623	"INJECTIVE_ON_IMAGE" > "HOLLight.hollight.INJECTIVE_ON_IMAGE"
kaliszyk@44639	1624	"INJECTIVE_MAP" > "HOLLightList.INJECTIVE_MAP"
obua@17644	1625	"INJECTIVE_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_LEFT_INVERSE"
kaliszyk@44639	1626	"INJECTIVE_IMAGE" > "HOLLight.hollight.INJECTIVE_IMAGE"
obua@17644	1627	"INJA_def" > "HOLLight.hollight.INJA_def"
obua@17644	1628	"INJA_INJ" > "HOLLight.hollight.INJA_INJ"
kaliszyk@44639	1629	"INFINITE_NONEMPTY" > "Infinite_Set.infinite_imp_nonempty"
obua@17644	1630	"INFINITE_IMAGE_INJ" > "HOLLight.hollight.INFINITE_IMAGE_INJ"
kaliszyk@44639	1631	"INFINITE_DIFF_FINITE" > "Infinite_Set.Diff_infinite_finite"
kaliszyk@44639	1632	"IND_SUC_def" > "HOLLight.hollight.IND_SUC_def"
kaliszyk@44639	1633	"IND_SUC_0_EXISTS" > "HOLLight.hollight.IND_SUC_0_EXISTS"
kaliszyk@44639	1634	"IND_0_def" > "HOLLight.hollight.IND_0_def"
obua@17644	1635	"IMP_EQ_CLAUSE" > "HOLLight.hollight.IMP_EQ_CLAUSE"
kaliszyk@44639	1636	"IMP_CONJ_ALT" > "HOLLight.hollight.IMP_CONJ_ALT"
obua@17644	1637	"IMP_CONJ" > "HOL.imp_conjL"
obua@17644	1638	"IMP_CLAUSES" > "HOLLight.hollight.IMP_CLAUSES"
kaliszyk@44639	1639	"IMAGE_o" > "Fun.image_compose"
kaliszyk@44639	1640	"IMAGE_UNIONS" > "HOLLight.hollight.IMAGE_UNIONS"
kaliszyk@44639	1641	"IMAGE_UNION" > "Set.image_Un"
kaliszyk@44639	1642	"IMAGE_SUBSET" > "Set.image_mono"
kaliszyk@44639	1643	"IMAGE_INTER_INJ" > "HOLLight.hollight.IMAGE_INTER_INJ"
kaliszyk@44639	1644	"IMAGE_INJECTIVE_IMAGE_OF_SUBSET" > "HOLLight.hollight.IMAGE_INJECTIVE_IMAGE_OF_SUBSET"
obua@17644	1645	"IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
obua@17644	1646	"IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
kaliszyk@44789	1647	"IMAGE_ID" > "Set.image_ident"
kaliszyk@44639	1648	"IMAGE_I" > "Fun.image_id"
kaliszyk@44639	1649	"IMAGE_EQ_EMPTY" > "Set.image_is_empty"
obua@17644	1650	"IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
obua@17644	1651	"IMAGE_DELETE_INJ" > "HOLLight.hollight.IMAGE_DELETE_INJ"
kaliszyk@44639	1652	"IMAGE_CONST" > "Set.image_constant_conv"
obua@17644	1653	"IMAGE_CLAUSES" > "HOLLight.hollight.IMAGE_CLAUSES"
obua@17644	1654	"HREAL_MUL_RZERO" > "HOLLight.hollight.HREAL_MUL_RZERO"
obua@17644	1655	"HREAL_MUL_LZERO" > "HOLLight.hollight.HREAL_MUL_LZERO"
obua@17644	1656	"HREAL_LE_MUL_RCANCEL_IMP" > "HOLLight.hollight.HREAL_LE_MUL_RCANCEL_IMP"
obua@17644	1657	"HREAL_LE_EXISTS_DEF" > "HOLLight.hollight.HREAL_LE_EXISTS_DEF"
obua@17644	1658	"HREAL_LE_ADD_RCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_RCANCEL"
obua@17644	1659	"HREAL_LE_ADD_LCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_LCANCEL"
obua@17644	1660	"HREAL_LE_ADD2" > "HOLLight.hollight.HREAL_LE_ADD2"
obua@17644	1661	"HREAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_RCANCEL"
obua@17644	1662	"HREAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_LCANCEL"
obua@17644	1663	"HREAL_ADD_RID" > "HOLLight.hollight.HREAL_ADD_RID"
obua@17644	1664	"HREAL_ADD_RDISTRIB" > "HOLLight.hollight.HREAL_ADD_RDISTRIB"
obua@17644	1665	"HREAL_ADD_AC" > "HOLLight.hollight.HREAL_ADD_AC"
kaliszyk@44639	1666	"HD_APPEND" > "List.hd_append"
obua@17644	1667	"HAS_SIZE_def" > "HOLLight.hollight.HAS_SIZE_def"
obua@17644	1668	"HAS_SIZE_UNIONS" > "HOLLight.hollight.HAS_SIZE_UNIONS"
obua@17644	1669	"HAS_SIZE_UNION" > "HOLLight.hollight.HAS_SIZE_UNION"
obua@17644	1670	"HAS_SIZE_SUC" > "HOLLight.hollight.HAS_SIZE_SUC"
obua@17644	1671	"HAS_SIZE_PRODUCT_DEPENDENT" > "HOLLight.hollight.HAS_SIZE_PRODUCT_DEPENDENT"
obua@17644	1672	"HAS_SIZE_PRODUCT" > "HOLLight.hollight.HAS_SIZE_PRODUCT"
obua@17644	1673	"HAS_SIZE_POWERSET" > "HOLLight.hollight.HAS_SIZE_POWERSET"
obua@17644	1674	"HAS_SIZE_NUMSEG_LT" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LT"
obua@17644	1675	"HAS_SIZE_NUMSEG_LE" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LE"
obua@17644	1676	"HAS_SIZE_NUMSEG_1" > "HOLLight.hollight.HAS_SIZE_NUMSEG_1"
obua@17644	1677	"HAS_SIZE_NUMSEG" > "HOLLight.hollight.HAS_SIZE_NUMSEG"
obua@17644	1678	"HAS_SIZE_INDEX" > "HOLLight.hollight.HAS_SIZE_INDEX"
kaliszyk@44639	1679	"HAS_SIZE_IMAGE_INJ_EQ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ_EQ"
obua@17644	1680	"HAS_SIZE_IMAGE_INJ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ"
obua@17644	1681	"HAS_SIZE_FUNSPACE" > "HOLLight.hollight.HAS_SIZE_FUNSPACE"
obua@17644	1682	"HAS_SIZE_FINITE_IMAGE" > "HOLLight.hollight.HAS_SIZE_FINITE_IMAGE"
kaliszyk@44639	1683	"HAS_SIZE_DIFF" > "HOLLight.hollight.HAS_SIZE_DIFF"
kaliszyk@44639	1684	"HAS_SIZE_CROSS" > "HOLLight.hollight.HAS_SIZE_CROSS"
obua@17644	1685	"HAS_SIZE_CLAUSES" > "HOLLight.hollight.HAS_SIZE_CLAUSES"
obua@17644	1686	"HAS_SIZE_CARD" > "HOLLight.hollight.HAS_SIZE_CARD"
kaliszyk@44639	1687	"HAS_SIZE_1" > "HOLLight.hollight.HAS_SIZE_1"
obua@17644	1688	"HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
kaliszyk@44639	1689	"GE_C" > "HOLLight.hollight.GE_C"
kaliszyk@44639	1690	"FUN_IN_IMAGE" > "Set.imageI"
nipkow@39535	1691	"FUN_EQ_THM" > "Fun.fun_eq_iff"
obua@17644	1692	"FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
obua@17644	1693	"FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
obua@17644	1694	"FST" > "Product_Type.fst_conv"
kaliszyk@44639	1695	"FORALL_UNWIND_THM2" > "HOL.simp_thms_41"
kaliszyk@44639	1696	"FORALL_UNWIND_THM1" > "HOL.simp_thms_42"
kaliszyk@44639	1697	"FORALL_UNCURRY" > "HOLLight.hollight.FORALL_UNCURRY"
kaliszyk@44639	1698	"FORALL_TRIPLED_THM" > "HOLLight.hollight.FORALL_TRIPLED_THM"
kaliszyk@44639	1699	"FORALL_SUBSET_IMAGE" > "HOLLight.hollight.FORALL_SUBSET_IMAGE"
obua@17644	1700	"FORALL_SIMP" > "HOL.simp_thms_35"
obua@17644	1701	"FORALL_PAIR_THM" > "Product_Type.split_paired_All"
kaliszyk@44639	1702	"FORALL_PAIRED_THM" > "HOLLight.hollight.FORALL_PAIRED_THM"
kaliszyk@44639	1703	"FORALL_NOT_THM" > "HOL.not_ex"
obua@17644	1704	"FORALL_IN_UNIONS" > "HOLLight.hollight.FORALL_IN_UNIONS"
kaliszyk@44639	1705	"FORALL_IN_INSERT" > "HOLLight.hollight.FORALL_IN_INSERT"
obua@17644	1706	"FORALL_IN_IMAGE" > "HOLLight.hollight.FORALL_IN_IMAGE"
kaliszyk@44639	1707	"FORALL_IN_GSPEC" > "HOLLight.hollight.FORALL_IN_GSPEC"
obua@17644	1708	"FORALL_IN_CLAUSES" > "HOLLight.hollight.FORALL_IN_CLAUSES"
obua@17644	1709	"FORALL_FINITE_INDEX" > "HOLLight.hollight.FORALL_FINITE_INDEX"
obua@17644	1710	"FORALL_BOOL_THM" > "Set.all_bool_eq"
obua@17644	1711	"FORALL_AND_THM" > "HOL.all_conj_distrib"
kaliszyk@44639	1712	"FORALL_ALL" > "HOLLightList.FORALL_ALL"
obua@17644	1713	"FNIL_def" > "HOLLight.hollight.FNIL_def"
obua@17644	1714	"FINREC_def" > "HOLLight.hollight.FINREC_def"
obua@17644	1715	"FINREC_UNIQUE_LEMMA" > "HOLLight.hollight.FINREC_UNIQUE_LEMMA"
obua@17644	1716	"FINREC_SUC_LEMMA" > "HOLLight.hollight.FINREC_SUC_LEMMA"
obua@17644	1717	"FINREC_FUN_LEMMA" > "HOLLight.hollight.FINREC_FUN_LEMMA"
obua@17644	1718	"FINREC_FUN" > "HOLLight.hollight.FINREC_FUN"
obua@17644	1719	"FINREC_EXISTS_LEMMA" > "HOLLight.hollight.FINREC_EXISTS_LEMMA"
obua@17644	1720	"FINREC_1_LEMMA" > "HOLLight.hollight.FINREC_1_LEMMA"
kaliszyk@44639	1721	"FINITE_UNION_IMP" > "Finite_Set.finite_UnI"
obua@17644	1722	"FINITE_UNIONS" > "HOLLight.hollight.FINITE_UNIONS"
kaliszyk@44639	1723	"FINITE_UNION" > "Finite_Set.finite_Un"
obua@17644	1724	"FINITE_SUPPORT_DELTA" > "HOLLight.hollight.FINITE_SUPPORT_DELTA"
obua@17644	1725	"FINITE_SUPPORT" > "HOLLight.hollight.FINITE_SUPPORT"
kaliszyk@44639	1726	"FINITE_SUM_IMAGE" > "HOLLight.hollight.FINITE_SUM_IMAGE"
obua@17644	1727	"FINITE_SUBSET_IMAGE_IMP" > "HOLLight.hollight.FINITE_SUBSET_IMAGE_IMP"
obua@17644	1728	"FINITE_SUBSET_IMAGE" > "HOLLight.hollight.FINITE_SUBSET_IMAGE"
kaliszyk@44639	1729	"FINITE_SUBSET" > "Finite_Set.finite_subset"
kaliszyk@44639	1730	"FINITE_SING" > "HOLLight.hollight.FINITE_SING"
obua@17644	1731	"FINITE_RESTRICT" > "HOLLight.hollight.FINITE_RESTRICT"
obua@17644	1732	"FINITE_RECURSION_DELETE" > "HOLLight.hollight.FINITE_RECURSION_DELETE"
obua@17644	1733	"FINITE_RECURSION" > "HOLLight.hollight.FINITE_RECURSION"
kaliszyk@44639	1734	"FINITE_REAL_INTERVAL" > "HOLLight.hollight.FINITE_REAL_INTERVAL"
obua@17644	1735	"FINITE_PRODUCT_DEPENDENT" > "HOLLight.hollight.FINITE_PRODUCT_DEPENDENT"
obua@17644	1736	"FINITE_PRODUCT" > "HOLLight.hollight.FINITE_PRODUCT"
obua@17644	1737	"FINITE_POWERSET" > "HOLLight.hollight.FINITE_POWERSET"
obua@17644	1738	"FINITE_NUMSEG_LT" > "HOLLight.hollight.FINITE_NUMSEG_LT"
obua@17644	1739	"FINITE_NUMSEG_LE" > "HOLLight.hollight.FINITE_NUMSEG_LE"
kaliszyk@44639	1740	"FINITE_NUMSEG" > "SetInterval.finite_atLeastAtMost"
kaliszyk@44639	1741	"FINITE_INTSEG" > "HOLLight.hollight.FINITE_INTSEG"
kaliszyk@44639	1742	"FINITE_INTER" > "Finite_Set.finite_Int"
kaliszyk@44639	1743	"FINITE_INSERT" > "Finite_Set.finite_insert"
kaliszyk@44639	1744	"FINITE_INDUCT_STRONG" > "Finite_Set.finite_induct"
kaliszyk@44639	1745	"FINITE_INDUCT_DELETE" > "HOLLight.hollight.FINITE_INDUCT_DELETE"
obua@17644	1746	"FINITE_INDEX_WORKS" > "HOLLight.hollight.FINITE_INDEX_WORKS"
obua@17644	1747	"FINITE_INDEX_NUMSEG" > "HOLLight.hollight.FINITE_INDEX_NUMSEG"
obua@17644	1748	"FINITE_INDEX_NUMBERS" > "HOLLight.hollight.FINITE_INDEX_NUMBERS"
kaliszyk@44639	1749	"FINITE_INDEX_INRANGE" > "HOLLight.hollight.FINITE_INDEX_INRANGE"
obua@17644	1750	"FINITE_INDEX_INJ" > "HOLLight.hollight.FINITE_INDEX_INJ"
obua@17644	1751	"FINITE_IMAGE_INJ_GENERAL" > "HOLLight.hollight.FINITE_IMAGE_INJ_GENERAL"
kaliszyk@44639	1752	"FINITE_IMAGE_INJ_EQ" > "HOLLight.hollight.FINITE_IMAGE_INJ_EQ"
obua@17644	1753	"FINITE_IMAGE_INJ" > "HOLLight.hollight.FINITE_IMAGE_INJ"
obua@17644	1754	"FINITE_IMAGE_IMAGE" > "HOLLight.hollight.FINITE_IMAGE_IMAGE"
obua@17644	1755	"FINITE_IMAGE_EXPAND" > "HOLLight.hollight.FINITE_IMAGE_EXPAND"
kaliszyk@44639	1756	"FINITE_IMAGE" > "Finite_Set.finite_imageI"
kaliszyk@44639	1757	"FINITE_HAS_SIZE" > "HOLLight.hollight.FINITE_HAS_SIZE"
obua@17644	1758	"FINITE_FUNSPACE" > "HOLLight.hollight.FINITE_FUNSPACE"
kaliszyk@44639	1759	"FINITE_FINITE_UNIONS" > "HOLLight.hollight.FINITE_FINITE_UNIONS"
kaliszyk@44639	1760	"FINITE_FINITE_PREIMAGE_GENERAL" > "HOLLight.hollight.FINITE_FINITE_PREIMAGE_GENERAL"
kaliszyk@44639	1761	"FINITE_FINITE_PREIMAGE" > "HOLLight.hollight.FINITE_FINITE_PREIMAGE"
obua@17644	1762	"FINITE_FINITE_IMAGE" > "HOLLight.hollight.FINITE_FINITE_IMAGE"
kaliszyk@44639	1763	"FINITE_EMPTY" > "Finite_Set.finite.emptyI"
kaliszyk@44639	1764	"FINITE_DIFF" > "Finite_Set.finite_Diff"
obua@17644	1765	"FINITE_DELETE_IMP" > "HOLLight.hollight.FINITE_DELETE_IMP"
obua@17644	1766	"FINITE_DELETE" > "HOLLight.hollight.FINITE_DELETE"
kaliszyk@44639	1767	"FINITE_CROSS" > "HOLLight.hollight.FINITE_CROSS"
kaliszyk@44639	1768	"FINITE_CART" > "HOLLight.hollight.FINITE_CART"
kaliszyk@44639	1769	"FILTER_MAP" > "List.filter_map"
kaliszyk@44639	1770	"FILTER_APPEND" > "List.filter_append"
obua@17644	1771	"FCONS_def" > "HOLLight.hollight.FCONS_def"
obua@17644	1772	"FCONS_UNDO" > "HOLLight.hollight.FCONS_UNDO"
kaliszyk@44639	1773	"FACT_NZ" > "Fact.fact_nonzero_nat"
kaliszyk@44639	1774	"FACT_MONO" > "Fact.fact_mono_nat"
kaliszyk@44639	1775	"FACT_LT" > "Fact.fact_gt_zero_nat"
kaliszyk@44639	1776	"FACT_LE" > "Fact.fact_ge_one_nat"
kaliszyk@44639	1777	"EX_MEM" > "HOLLightList.EX_MEM"
kaliszyk@44639	1778	"EX_IMP" > "HOLLightList.EX_IMP"
kaliszyk@44639	1779	"EXTENSION" > "Set.set_eq_iff"
kaliszyk@44639	1780	"EXP_ZERO" > "Power.power_0_left"
kaliszyk@44639	1781	"EXP_ONE" > "Power.monoid_mult_class.power_one"
kaliszyk@44639	1782	"EXP_MULT" > "Power.monoid_mult_class.power_mult"
kaliszyk@44639	1783	"EXP_MONO_LT_IMP" > "HOLLight.hollight.EXP_MONO_LT_IMP"
kaliszyk@44639	1784	"EXP_MONO_LT" > "HOLLight.hollight.EXP_MONO_LT"
kaliszyk@44639	1785	"EXP_MONO_LE_IMP" > "HOLLight.hollight.EXP_MONO_LE_IMP"
kaliszyk@44639	1786	"EXP_MONO_LE" > "HOLLight.hollight.EXP_MONO_LE"
kaliszyk@44639	1787	"EXP_MONO_EQ" > "HOLLight.hollight.EXP_MONO_EQ"
obua@17644	1788	"EXP_LT_0" > "HOLLight.hollight.EXP_LT_0"
kaliszyk@44639	1789	"EXP_EQ_1" > "HOLLight.hollight.EXP_EQ_1"
kaliszyk@44639	1790	"EXP_EQ_0" > "Power.power_eq_0_iff"
kaliszyk@44639	1791	"EXP_ADD" > "Power.monoid_mult_class.power_add"
kaliszyk@44639	1792	"EXP_2" > "Nat_Numeral.monoid_mult_class.power2_eq_square"
kaliszyk@44639	1793	"EXP_1" > "Power.monoid_mult_class.power_one_right"
kaliszyk@44639	1794	"EXISTS_UNIQUE_THM" > "HOLLightCompat.EXISTS_UNIQUE_THM"
obua@17644	1795	"EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
obua@17644	1796	"EXISTS_UNIQUE_ALT" > "HOLLight.hollight.EXISTS_UNIQUE_ALT"
obua@17644	1797	"EXISTS_UNIQUE" > "HOL.Ex1_def"
kaliszyk@44639	1798	"EXISTS_UNCURRY" > "HOLLight.hollight.EXISTS_UNCURRY"
kaliszyk@44639	1799	"EXISTS_TRIPLED_THM" > "HOLLight.hollight.EXISTS_TRIPLED_THM"
obua@17644	1800	"EXISTS_THM" > "HOL4Setup.EXISTS_DEF"
kaliszyk@44639	1801	"EXISTS_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_SUBSET_IMAGE"
obua@17644	1802	"EXISTS_SIMP" > "HOL.simp_thms_36"
obua@17644	1803	"EXISTS_REFL" > "HOL.simp_thms_37"
obua@17644	1804	"EXISTS_PAIR_THM" > "Product_Type.split_paired_Ex"
kaliszyk@44639	1805	"EXISTS_PAIRED_THM" > "HOLLight.hollight.EXISTS_PAIRED_THM"
obua@17644	1806	"EXISTS_OR_THM" > "HOL.ex_disj_distrib"
obua@17644	1807	"EXISTS_ONE_REP" > "HOLLight.hollight.EXISTS_ONE_REP"
kaliszyk@44639	1808	"EXISTS_NOT_THM" > "HOL.not_all"
kaliszyk@44639	1809	"EXISTS_IN_UNIONS" > "HOLLight.hollight.EXISTS_IN_UNIONS"
kaliszyk@44639	1810	"EXISTS_IN_INSERT" > "HOLLight.hollight.EXISTS_IN_INSERT"
obua@17644	1811	"EXISTS_IN_IMAGE" > "HOLLight.hollight.EXISTS_IN_IMAGE"
kaliszyk@44639	1812	"EXISTS_IN_GSPEC" > "HOLLight.hollight.EXISTS_IN_GSPEC"
obua@17644	1813	"EXISTS_IN_CLAUSES" > "HOLLight.hollight.EXISTS_IN_CLAUSES"
kaliszyk@44639	1814	"EXISTS_FINITE_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_FINITE_SUBSET_IMAGE"
kaliszyk@44639	1815	"EXISTS_EX" > "HOLLightList.EXISTS_EX"
obua@17644	1816	"EXISTS_BOOL_THM" > "Set.ex_bool_eq"
obua@17644	1817	"EXCLUDED_MIDDLE" > "HOLLight.hollight.EXCLUDED_MIDDLE"
kaliszyk@44639	1818	"EVEN_SUB" > "HOLLight.hollight.EVEN_SUB"
obua@17644	1819	"EVEN_OR_ODD" > "HOLLight.hollight.EVEN_OR_ODD"
obua@17644	1820	"EVEN_ODD_DECOMPOSITION" > "HOLLight.hollight.EVEN_ODD_DECOMPOSITION"
kaliszyk@44639	1821	"EVEN_MULT" > "Parity.even_product_nat"
obua@17644	1822	"EVEN_MOD" > "HOLLight.hollight.EVEN_MOD"
obua@17644	1823	"EVEN_EXP" > "HOLLight.hollight.EVEN_EXP"
obua@17644	1824	"EVEN_EXISTS_LEMMA" > "HOLLight.hollight.EVEN_EXISTS_LEMMA"
kaliszyk@44639	1825	"EVEN_EXISTS" > "Parity.even_mult_two_ex"
obua@17644	1826	"EVEN_DOUBLE" > "HOLLight.hollight.EVEN_DOUBLE"
obua@17644	1827	"EVEN_AND_ODD" > "HOLLight.hollight.EVEN_AND_ODD"
kaliszyk@44639	1828	"EVEN_ADD" > "Parity.even_add"
obua@17644	1829	"EQ_UNIV" > "HOLLight.hollight.EQ_UNIV"
kaliszyk@44639	1830	"EQ_TRANS" > "HOL.trans"
kaliszyk@44639	1831	"EQ_SYM_EQ" > "HOL.eq_ac_1"
kaliszyk@44639	1832	"EQ_SYM" > "HOL.eq_reflection"
kaliszyk@44639	1833	"EQ_REFL" > "HOL.refl"
obua@17644	1834	"EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
kaliszyk@44639	1835	"EQ_MULT_LCANCEL" > "Numeral_Simprocs.nat_mult_eq_cancel_disj"
kaliszyk@44639	1836	"EQ_IMP_LE" > "Nat.eq_imp_le"
kaliszyk@44639	1837	"EQ_EXT" > "HOL.eq_reflection"
kaliszyk@44639	1838	"EQ_EXP" > "HOLLight.hollight.EQ_EXP"
obua@17644	1839	"EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
obua@17644	1840	"EQ_ADD_RCANCEL_0" > "HOLLight.hollight.EQ_ADD_RCANCEL_0"
kaliszyk@44639	1841	"EQ_ADD_RCANCEL" > "Groups.cancel_semigroup_add_class.add_right_cancel"
obua@17644	1842	"EQ_ADD_LCANCEL_0" > "HOLLight.hollight.EQ_ADD_LCANCEL_0"
kaliszyk@44639	1843	"EQ_ADD_LCANCEL" > "Groups.cancel_semigroup_add_class.add_left_cancel"
obua@17644	1844	"EMPTY_UNIONS" > "HOLLight.hollight.EMPTY_UNIONS"
kaliszyk@44639	1845	"EMPTY_UNION" > "Lattices.bounded_lattice_bot_class.sup_eq_bot_iff"
kaliszyk@44639	1846	"EMPTY_SUBSET" > "Orderings.bot_class.bot_least"
obua@17644	1847	"EMPTY_NOT_UNIV" > "HOLLight.hollight.EMPTY_NOT_UNIV"
obua@17644	1848	"EMPTY_GSPEC" > "HOLLight.hollight.EMPTY_GSPEC"
kaliszyk@44639	1849	"EMPTY_DIFF" > "Set.empty_Diff"
obua@17644	1850	"EMPTY_DELETE" > "HOLLight.hollight.EMPTY_DELETE"
kaliszyk@44639	1851	"EL_CONS" > "List.nth_Cons'"
kaliszyk@44639	1852	"EL_APPEND" > "List.nth_append"
obua@17644	1853	"DIV_UNIQ" > "HOLLight.hollight.DIV_UNIQ"
kaliszyk@44639	1854	"DIV_REFL" > "Divides.semiring_div_class.div_self"
obua@17644	1855	"DIV_MUL_LE" > "HOLLight.hollight.DIV_MUL_LE"
obua@17644	1856	"DIV_MULT2" > "HOLLight.hollight.DIV_MULT2"
obua@17644	1857	"DIV_MONO_LT" > "HOLLight.hollight.DIV_MONO_LT"
obua@17644	1858	"DIV_MONO2" > "HOLLight.hollight.DIV_MONO2"
obua@17644	1859	"DIV_MONO" > "HOLLight.hollight.DIV_MONO"
obua@17644	1860	"DIV_MOD" > "HOLLight.hollight.DIV_MOD"
kaliszyk@44639	1861	"DIV_LT" > "Divides.div_less"
obua@17644	1862	"DIV_LE_EXCLUSION" > "HOLLight.hollight.DIV_LE_EXCLUSION"
obua@17644	1863	"DIV_LE" > "HOLLight.hollight.DIV_LE"
obua@17644	1864	"DIV_EQ_EXCLUSION" > "HOLLight.hollight.DIV_EQ_EXCLUSION"
obua@17644	1865	"DIV_EQ_0" > "HOLLight.hollight.DIV_EQ_0"
obua@17644	1866	"DIV_DIV" > "HOLLight.hollight.DIV_DIV"
obua@17644	1867	"DIV_ADD_MOD" > "HOLLight.hollight.DIV_ADD_MOD"
obua@17644	1868	"DIVMOD_UNIQ_LEMMA" > "HOLLight.hollight.DIVMOD_UNIQ_LEMMA"
obua@17644	1869	"DIVMOD_UNIQ" > "HOLLight.hollight.DIVMOD_UNIQ"
obua@17644	1870	"DIVMOD_EXIST_0" > "HOLLight.hollight.DIVMOD_EXIST_0"
obua@17644	1871	"DIVMOD_EXIST" > "HOLLight.hollight.DIVMOD_EXIST"
obua@17644	1872	"DIVMOD_ELIM_THM" > "HOLLight.hollight.DIVMOD_ELIM_THM"
obua@17644	1873	"DIVISION" > "HOLLight.hollight.DIVISION"
obua@17644	1874	"DIST_TRIANGLE_LE" > "HOLLight.hollight.DIST_TRIANGLE_LE"
obua@17644	1875	"DIST_TRIANGLES_LE" > "HOLLight.hollight.DIST_TRIANGLES_LE"
obua@17644	1876	"DIST_SYM" > "HOLLight.hollight.DIST_SYM"
obua@17644	1877	"DIST_RZERO" > "HOLLight.hollight.DIST_RZERO"
obua@17644	1878	"DIST_RMUL" > "HOLLight.hollight.DIST_RMUL"
obua@17644	1879	"DIST_REFL" > "HOLLight.hollight.DIST_REFL"
obua@17644	1880	"DIST_RADD_0" > "HOLLight.hollight.DIST_RADD_0"
obua@17644	1881	"DIST_RADD" > "HOLLight.hollight.DIST_RADD"
obua@17644	1882	"DIST_LZERO" > "HOLLight.hollight.DIST_LZERO"
obua@17644	1883	"DIST_LMUL" > "HOLLight.hollight.DIST_LMUL"
obua@17644	1884	"DIST_LE_CASES" > "HOLLight.hollight.DIST_LE_CASES"
obua@17644	1885	"DIST_LADD_0" > "HOLLight.hollight.DIST_LADD_0"
obua@17644	1886	"DIST_LADD" > "HOLLight.hollight.DIST_LADD"
obua@17644	1887	"DIST_EQ_0" > "HOLLight.hollight.DIST_EQ_0"
obua@17644	1888	"DIST_ELIM_THM" > "HOLLight.hollight.DIST_ELIM_THM"
kaliszyk@44639	1889	"DISJ_SYM" > "Groebner_Basis.dnf_4"
kaliszyk@44639	1890	"DISJ_ASSOC" > "HOL.disj_ac_3"
obua@17644	1891	"DISJ_ACI" > "HOLLight.hollight.DISJ_ACI"
obua@17644	1892	"DISJOINT_UNION" > "HOLLight.hollight.DISJOINT_UNION"
obua@17644	1893	"DISJOINT_SYM" > "HOLLight.hollight.DISJOINT_SYM"
obua@17644	1894	"DISJOINT_NUMSEG" > "HOLLight.hollight.DISJOINT_NUMSEG"
obua@17644	1895	"DISJOINT_INSERT" > "HOLLight.hollight.DISJOINT_INSERT"
obua@17644	1896	"DISJOINT_EMPTY_REFL" > "HOLLight.hollight.DISJOINT_EMPTY_REFL"
obua@17644	1897	"DISJOINT_EMPTY" > "HOLLight.hollight.DISJOINT_EMPTY"
obua@17644	1898	"DISJOINT_DELETE_SYM" > "HOLLight.hollight.DISJOINT_DELETE_SYM"
kaliszyk@44639	1899	"DIMINDEX_UNIV" > "HOLLight.hollight.DIMINDEX_UNIV"
kaliszyk@44639	1900	"DIMINDEX_UNIQUE" > "HOLLight.hollight.DIMINDEX_UNIQUE"
obua@17644	1901	"DIMINDEX_NONZERO" > "HOLLight.hollight.DIMINDEX_NONZERO"
obua@17644	1902	"DIMINDEX_GE_1" > "HOLLight.hollight.DIMINDEX_GE_1"
obua@17644	1903	"DIMINDEX_FINITE_IMAGE" > "HOLLight.hollight.DIMINDEX_FINITE_IMAGE"
kaliszyk@44639	1904	"DIFF_UNIV" > "Set.Diff_UNIV"
kaliszyk@44639	1905	"DIFF_INTERS" > "HOLLight.hollight.DIFF_INTERS"
kaliszyk@44639	1906	"DIFF_INSERT" > "Set.Diff_insert2"
kaliszyk@44639	1907	"DIFF_EQ_EMPTY" > "Set.Diff_cancel"
kaliszyk@44639	1908	"DIFF_EMPTY" > "Set.Diff_empty"
kaliszyk@44639	1909	"DIFF_DIFF" > "Set.Diff_idemp"
obua@17644	1910	"DEST_REC_INJ" > "HOLLight.hollight.recspace._dest_rec_inject"
obua@17644	1911	"DELETE_SUBSET" > "HOLLight.hollight.DELETE_SUBSET"
obua@17644	1912	"DELETE_NON_ELEMENT" > "HOLLight.hollight.DELETE_NON_ELEMENT"
obua@17644	1913	"DELETE_INTER" > "HOLLight.hollight.DELETE_INTER"
obua@17644	1914	"DELETE_INSERT" > "HOLLight.hollight.DELETE_INSERT"
obua@17644	1915	"DELETE_DELETE" > "HOLLight.hollight.DELETE_DELETE"
obua@17644	1916	"DELETE_COMM" > "HOLLight.hollight.DELETE_COMM"
kaliszyk@44639	1917	"DEF_~" > "Groebner_Basis.bool_simps_19"
kaliszyk@44639	1918	"DEF_vector" > "HOLLight.hollight.DEF_vector"
obua@17644	1919	"DEF_treal_of_num" > "HOLLight.hollight.DEF_treal_of_num"
obua@17644	1920	"DEF_treal_neg" > "HOLLight.hollight.DEF_treal_neg"
obua@17644	1921	"DEF_treal_mul" > "HOLLight.hollight.DEF_treal_mul"
obua@17644	1922	"DEF_treal_le" > "HOLLight.hollight.DEF_treal_le"
obua@17644	1923	"DEF_treal_inv" > "HOLLight.hollight.DEF_treal_inv"
obua@17644	1924	"DEF_treal_eq" > "HOLLight.hollight.DEF_treal_eq"
obua@17644	1925	"DEF_treal_add" > "HOLLight.hollight.DEF_treal_add"
obua@17644	1926	"DEF_tailadmissible" > "HOLLight.hollight.DEF_tailadmissible"
obua@17644	1927	"DEF_support" > "HOLLight.hollight.DEF_support"
obua@17644	1928	"DEF_superadmissible" > "HOLLight.hollight.DEF_superadmissible"
obua@17644	1929	"DEF_sum" > "HOLLight.hollight.DEF_sum"
obua@17644	1930	"DEF_sndcart" > "HOLLight.hollight.DEF_sndcart"
kaliszyk@44639	1931	"DEF_set_of_list" > "HOLLightList.DEF_set_of_list"
kaliszyk@44639	1932	"DEF_rem" > "HOLLight.hollight.DEF_rem"
obua@17644	1933	"DEF_real_sub" > "HOLLight.hollight.DEF_real_sub"
kaliszyk@44639	1934	"DEF_real_sgn" > "HOLLight.hollight.DEF_real_sgn"
obua@17644	1935	"DEF_real_pow" > "HOLLight.hollight.DEF_real_pow"
obua@17644	1936	"DEF_real_of_num" > "HOLLight.hollight.DEF_real_of_num"
obua@17644	1937	"DEF_real_neg" > "HOLLight.hollight.DEF_real_neg"
obua@17644	1938	"DEF_real_mul" > "HOLLight.hollight.DEF_real_mul"
kaliszyk@44639	1939	"DEF_real_mod" > "HOLLight.hollight.DEF_real_mod"
obua@17644	1940	"DEF_real_min" > "HOLLight.hollight.DEF_real_min"
obua@17644	1941	"DEF_real_max" > "HOLLight.hollight.DEF_real_max"
obua@17644	1942	"DEF_real_lt" > "HOLLight.hollight.DEF_real_lt"
obua@17644	1943	"DEF_real_le" > "HOLLight.hollight.DEF_real_le"
obua@17644	1944	"DEF_real_inv" > "HOLLight.hollight.DEF_real_inv"
obua@17644	1945	"DEF_real_gt" > "HOLLight.hollight.DEF_real_gt"
obua@17644	1946	"DEF_real_ge" > "HOLLight.hollight.DEF_real_ge"
obua@17644	1947	"DEF_real_div" > "HOLLight.hollight.DEF_real_div"
obua@17644	1948	"DEF_real_add" > "HOLLight.hollight.DEF_real_add"
obua@17644	1949	"DEF_real_abs" > "HOLLight.hollight.DEF_real_abs"
obua@17644	1950	"DEF_pastecart" > "HOLLight.hollight.DEF_pastecart"
obua@17644	1951	"DEF_pairwise" > "HOLLight.hollight.DEF_pairwise"
kaliszyk@44639	1952	"DEF_o" > "Fun.comp_def"
kaliszyk@44639	1953	"DEF_num_of_int" > "HOLLight.hollight.DEF_num_of_int"
kaliszyk@44639	1954	"DEF_num_mod" > "HOLLight.hollight.DEF_num_mod"
kaliszyk@44639	1955	"DEF_num_gcd" > "HOLLight.hollight.DEF_num_gcd"
kaliszyk@44639	1956	"DEF_num_divides" > "HOLLight.hollight.DEF_num_divides"
kaliszyk@44639	1957	"DEF_num_coprime" > "HOLLight.hollight.DEF_num_coprime"
obua@17644	1958	"DEF_nsum" > "HOLLight.hollight.DEF_nsum"
obua@17644	1959	"DEF_neutral" > "HOLLight.hollight.DEF_neutral"
obua@17644	1960	"DEF_nadd_rinv" > "HOLLight.hollight.DEF_nadd_rinv"
obua@17644	1961	"DEF_nadd_of_num" > "HOLLight.hollight.DEF_nadd_of_num"
obua@17644	1962	"DEF_nadd_mul" > "HOLLight.hollight.DEF_nadd_mul"
obua@17644	1963	"DEF_nadd_le" > "HOLLight.hollight.DEF_nadd_le"
obua@17644	1964	"DEF_nadd_inv" > "HOLLight.hollight.DEF_nadd_inv"
obua@17644	1965	"DEF_nadd_eq" > "HOLLight.hollight.DEF_nadd_eq"
obua@17644	1966	"DEF_nadd_add" > "HOLLight.hollight.DEF_nadd_add"
obua@17644	1967	"DEF_monoidal" > "HOLLight.hollight.DEF_monoidal"
obua@17644	1968	"DEF_minimal" > "HOLLight.hollight.DEF_minimal"
obua@17644	1969	"DEF_lambda" > "HOLLight.hollight.DEF_lambda"
obua@17644	1970	"DEF_iterate" > "HOLLight.hollight.DEF_iterate"
obua@17644	1971	"DEF_is_nadd" > "HOLLight.hollight.DEF_is_nadd"
kaliszyk@44639	1972	"DEF_integer" > "HOLLight.hollight.DEF_integer"
obua@17644	1973	"DEF_int_sub" > "HOLLight.hollight.DEF_int_sub"
kaliszyk@44639	1974	"DEF_int_sgn" > "HOLLight.hollight.DEF_int_sgn"
obua@17644	1975	"DEF_int_pow" > "HOLLight.hollight.DEF_int_pow"
obua@17644	1976	"DEF_int_of_num" > "HOLLight.hollight.DEF_int_of_num"
obua@17644	1977	"DEF_int_neg" > "HOLLight.hollight.DEF_int_neg"
obua@17644	1978	"DEF_int_mul" > "HOLLight.hollight.DEF_int_mul"
kaliszyk@44639	1979	"DEF_int_mod" > "HOLLight.hollight.DEF_int_mod"
obua@17644	1980	"DEF_int_min" > "HOLLight.hollight.DEF_int_min"
obua@17644	1981	"DEF_int_max" > "HOLLight.hollight.DEF_int_max"
obua@17644	1982	"DEF_int_lt" > "HOLLight.hollight.DEF_int_lt"
obua@17644	1983	"DEF_int_le" > "HOLLight.hollight.DEF_int_le"
obua@17644	1984	"DEF_int_gt" > "HOLLight.hollight.DEF_int_gt"
obua@17644	1985	"DEF_int_ge" > "HOLLight.hollight.DEF_int_ge"
kaliszyk@44639	1986	"DEF_int_gcd" > "HOLLight.hollight.DEF_int_gcd"
kaliszyk@44639	1987	"DEF_int_divides" > "HOLLight.hollight.DEF_int_divides"
kaliszyk@44639	1988	"DEF_int_coprime" > "HOLLight.hollight.DEF_int_coprime"
obua@17644	1989	"DEF_int_add" > "HOLLight.hollight.DEF_int_add"
obua@17644	1990	"DEF_int_abs" > "HOLLight.hollight.DEF_int_abs"
obua@17644	1991	"DEF_hreal_of_num" > "HOLLight.hollight.DEF_hreal_of_num"
obua@17644	1992	"DEF_hreal_mul" > "HOLLight.hollight.DEF_hreal_mul"
obua@17644	1993	"DEF_hreal_le" > "HOLLight.hollight.DEF_hreal_le"
obua@17644	1994	"DEF_hreal_inv" > "HOLLight.hollight.DEF_hreal_inv"
obua@17644	1995	"DEF_hreal_add" > "HOLLight.hollight.DEF_hreal_add"
obua@17644	1996	"DEF_fstcart" > "HOLLight.hollight.DEF_fstcart"
kaliszyk@44639	1997	"DEF_div" > "HOLLight.hollight.DEF_div"
obua@17644	1998	"DEF_dist" > "HOLLight.hollight.DEF_dist"
obua@17644	1999	"DEF_dimindex" > "HOLLight.hollight.DEF_dimindex"
obua@17644	2000	"DEF_admissible" > "HOLLight.hollight.DEF_admissible"
kaliszyk@44639	2001	"DEF__star_" > "HOLLightCompat.DEF__star_"
kaliszyk@44639	2002	"DEF__slash__backslash_" > "HOLLightCompat.DEF__slash__backslash_"
kaliszyk@44639	2003	"DEF__questionmark__exclamationmark_" > "HOLLightCompat.EXISTS_UNIQUE_THM"
obua@17644	2004	"DEF__questionmark_" > "HOL.Ex_def"
kaliszyk@44639	2005	"DEF__lessthan__equal__c" > "HOLLight.hollight.DEF__lessthan__equal__c"
kaliszyk@44639	2006	"DEF__lessthan__equal_" > "HOLLightCompat.DEF__lessthan__equal_"
kaliszyk@44639	2007	"DEF__lessthan__c" > "HOLLight.hollight.DEF__lessthan__c"
kaliszyk@44639	2008	"DEF__lessthan_" > "HOLLightCompat.DEF__lessthan_"
kaliszyk@44639	2009	"DEF__greaterthan__equal__c" > "HOLLight.hollight.DEF__greaterthan__equal__c"
kaliszyk@44639	2010	"DEF__greaterthan__equal_" > "HOLLightCompat.DEF__greaterthan__equal_"
kaliszyk@44639	2011	"DEF__greaterthan__c" > "HOLLight.hollight.DEF__greaterthan__c"
kaliszyk@44639	2012	"DEF__greaterthan_" > "HOLLightCompat.DEF__greaterthan_"
obua@17644	2013	"DEF__exclamationmark_" > "HOL.All_def"
kaliszyk@44639	2014	"DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_"
obua@17644	2015	"DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
kaliszyk@44639	2016	"DEF__equal__c" > "HOLLight.hollight.DEF__equal__c"
kaliszyk@44639	2017	"DEF__dot__dot_" > "HOLLightCompat.DEF__dot__dot_"
obua@17644	2018	"DEF__backslash__slash_" > "HOL.or_def"
kaliszyk@44639	2019	"DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN"
kaliszyk@44639	2020	"DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN"
kaliszyk@44639	2021	"DEF__MATCH" > "HOLLight.hollight.DEF__MATCH"
kaliszyk@44639	2022	"DEF__GUARDED_PATTERN" > "HOLLight.hollight.DEF__GUARDED_PATTERN"
kaliszyk@44639	2023	"DEF__FUNCTION" > "HOLLight.hollight.DEF__FUNCTION"
obua@17644	2024	"DEF__FALSITY_" > "HOLLight.hollight.DEF__FALSITY_"
kaliszyk@44639	2025	"DEF__11937" > "HOLLight.hollight.DEF__11937"
obua@17644	2026	"DEF_ZRECSPACE" > "HOLLight.hollight.DEF_ZRECSPACE"
obua@17644	2027	"DEF_ZCONSTR" > "HOLLight.hollight.DEF_ZCONSTR"
obua@17644	2028	"DEF_ZBOT" > "HOLLight.hollight.DEF_ZBOT"
kaliszyk@44639	2029	"DEF_WF" > "HOLLightCompat.DEF_WF"
kaliszyk@44639	2030	"DEF_UNIV" > "HOLLightCompat.DEF_UNIV"
kaliszyk@44639	2031	"DEF_UNIONS" > "HOLLightCompat.DEF_UNIONS"
kaliszyk@44639	2032	"DEF_UNION" > "HOLLightCompat.DEF_UNION"
obua@17644	2033	"DEF_UNCURRY" > "HOLLight.hollight.DEF_UNCURRY"
obua@17644	2034	"DEF_T" > "HOL.True_def"
obua@17644	2035	"DEF_SURJ" > "HOLLight.hollight.DEF_SURJ"
kaliszyk@44639	2036	"DEF_SUBSET" > "HOLLightCompat.DEF_SUBSET"
kaliszyk@44639	2037	"DEF_SND" > "HOLLightCompat.DEF_SND"
obua@17644	2038	"DEF_SING" > "HOLLight.hollight.DEF_SING"
kaliszyk@44639	2039	"DEF_SETSPEC" > "HOLLightCompat.SETSPEC_def"
kaliszyk@44639	2040	"DEF_REVERSE" > "HOLLightList.DEF_REVERSE"
obua@17644	2041	"DEF_REST" > "HOLLight.hollight.DEF_REST"
kaliszyk@44639	2042	"DEF_REPLICATE" > "HOLLightList.DEF_REPLICATE"
kaliszyk@44639	2043	"DEF_PSUBSET" > "HOLLightCompat.DEF_PSUBSET"
kaliszyk@44639	2044	"DEF_PRE" > "HOLLightCompat.DEF_PRE"
obua@17644	2045	"DEF_PASSOC" > "HOLLight.hollight.DEF_PASSOC"
obua@17644	2046	"DEF_PAIRWISE" > "HOLLight.hollight.DEF_PAIRWISE"
obua@17644	2047	"DEF_ONTO" > "Fun.surj_def"
kaliszyk@44639	2048	"DEF_ONE_ONE" > "HOLLightCompat.DEF_ONE_ONE"
kaliszyk@44639	2049	"DEF_ODD" > "HOLLightCompat.DEF_ODD"
kaliszyk@44639	2050	"DEF_NUM_REP" > "HOLLight.hollight.DEF_NUM_REP"
obua@17644	2051	"DEF_NUMSUM" > "HOLLight.hollight.DEF_NUMSUM"
obua@17644	2052	"DEF_NUMSND" > "HOLLight.hollight.DEF_NUMSND"
obua@17644	2053	"DEF_NUMRIGHT" > "HOLLight.hollight.DEF_NUMRIGHT"
obua@17644	2054	"DEF_NUMPAIR" > "HOLLight.hollight.DEF_NUMPAIR"
obua@17644	2055	"DEF_NUMLEFT" > "HOLLight.hollight.DEF_NUMLEFT"
obua@17644	2056	"DEF_NUMFST" > "HOLLight.hollight.DEF_NUMFST"
kaliszyk@44639	2057	"DEF_NUMERAL" > "HOLLightCompat.NUMERAL_def"
kaliszyk@44639	2058	"DEF_NULL" > "HOLLightList.DEF_NULL"
kaliszyk@44639	2059	"DEF_MOD" > "HOLLightCompat.DEF_MOD"
kaliszyk@44639	2060	"DEF_MIN" > "Orderings.ord_class.min_def"
kaliszyk@44639	2061	"DEF_MEM" > "HOLLightList.DEF_MEM"
kaliszyk@44639	2062	"DEF_MEASURE" > "HOLLightCompat.MEASURE_def"
kaliszyk@44639	2063	"DEF_MAX" > "Orderings.ord_class.max_def"
kaliszyk@44639	2064	"DEF_MAP" > "HOLLightList.DEF_MAP"
obua@17644	2065	"DEF_LET_END" > "HOLLight.hollight.DEF_LET_END"
kaliszyk@44639	2066	"DEF_LET" > "HOLLightCompat.LET_def"
kaliszyk@44639	2067	"DEF_LENGTH" > "HOLLightList.DEF_LENGTH"
kaliszyk@44639	2068	"DEF_LAST" > "HOLLightList.DEF_LAST"
obua@17644	2069	"DEF_ITSET" > "HOLLight.hollight.DEF_ITSET"
kaliszyk@44639	2070	"DEF_ITLIST" > "HOLLightList.DEF_ITLIST"
obua@17644	2071	"DEF_ISO" > "HOLLight.hollight.DEF_ISO"
kaliszyk@44639	2072	"DEF_INTERS" > "HOLLightCompat.DEF_INTERS"
kaliszyk@44639	2073	"DEF_INTER" > "HOLLightCompat.DEF_INTER"
kaliszyk@44639	2074	"DEF_INSERT" > "HOLLightCompat.DEF_INSERT"
obua@17644	2075	"DEF_INJP" > "HOLLight.hollight.DEF_INJP"
obua@17644	2076	"DEF_INJN" > "HOLLight.hollight.DEF_INJN"
obua@17644	2077	"DEF_INJF" > "HOLLight.hollight.DEF_INJF"
obua@17644	2078	"DEF_INJA" > "HOLLight.hollight.DEF_INJA"
obua@17644	2079	"DEF_INJ" > "HOLLight.hollight.DEF_INJ"
kaliszyk@44639	2080	"DEF_INFINITE" > "HOLLightCompat.DEF_INFINITE"
kaliszyk@44639	2081	"DEF_IND_SUC" > "HOLLight.hollight.DEF_IND_SUC"
kaliszyk@44639	2082	"DEF_IND_0" > "HOLLight.hollight.DEF_IND_0"
kaliszyk@44639	2083	"DEF_IN" > "Set.mem_def"
kaliszyk@44639	2084	"DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE"
obua@17644	2085	"DEF_I" > "Fun.id_apply"
obua@17644	2086	"DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
kaliszyk@44639	2087	"DEF_GSPEC" > "HOLLightCompat.DEF_GSPEC"
kaliszyk@44639	2088	"DEF_GEQ" > "HOLLightCompat.DEF_GEQ"
kaliszyk@44639	2089	"DEF_GABS" > "HOLLightCompat.DEF_GABS"
kaliszyk@44639	2090	"DEF_FST" > "HOLLightCompat.DEF_FST"
obua@17644	2091	"DEF_FNIL" > "HOLLight.hollight.DEF_FNIL"
obua@17644	2092	"DEF_FINREC" > "HOLLight.hollight.DEF_FINREC"
kaliszyk@44639	2093	"DEF_FINITE" > "HOLLightCompat.DEF_FINITE"
kaliszyk@44639	2094	"DEF_FILTER" > "HOLLightList.DEF_FILTER"
obua@17644	2095	"DEF_FCONS" > "HOLLight.hollight.DEF_FCONS"
kaliszyk@44639	2096	"DEF_FACT" > "HOLLightCompat.DEF_FACT"
obua@17644	2097	"DEF_F" > "HOL.False_def"
kaliszyk@44639	2098	"DEF_EXP" > "HOLLightCompat.DEF_EXP"
kaliszyk@44639	2099	"DEF_EX" > "HOLLightList.DEF_EX"
kaliszyk@44639	2100	"DEF_EVEN" > "HOLLightCompat.DEF_EVEN"
kaliszyk@44639	2101	"DEF_EMPTY" > "HOLLightCompat.DEF_EMPTY"
kaliszyk@44639	2102	"DEF_EL" > "HOLLightList.DEF_EL"
kaliszyk@44639	2103	"DEF_DIV" > "HOLLightCompat.DEF_DIV"
kaliszyk@44639	2104	"DEF_DISJOINT" > "HOLLightCompat.DEF_DISJOINT"
kaliszyk@44639	2105	"DEF_DIFF" > "HOLLightCompat.DEF_DIFF"
kaliszyk@44639	2106	"DEF_DELETE" > "HOLLightCompat.DEF_DELETE"
obua@17644	2107	"DEF_DECIMAL" > "HOLLight.hollight.DEF_DECIMAL"
kaliszyk@44639	2108	"DEF_CURRY" > "Product_Type.curry_conv"
kaliszyk@44639	2109	"DEF_CROSS" > "HOLLight.hollight.DEF_CROSS"
obua@17644	2110	"DEF_COUNTABLE" > "HOLLight.hollight.DEF_COUNTABLE"
obua@17644	2111	"DEF_CONSTR" > "HOLLight.hollight.DEF_CONSTR"
kaliszyk@44639	2112	"DEF_COND" > "HOLLightCompat.COND_DEF"
kaliszyk@44639	2113	"DEF_CHOICE" > "HOLLightCompat.DEF_CHOICE"
obua@17644	2114	"DEF_CASEWISE" > "HOLLight.hollight.DEF_CASEWISE"
obua@17644	2115	"DEF_CARD" > "HOLLight.hollight.DEF_CARD"
kaliszyk@44639	2116	"DEF_BUTLAST" > "HOLLightList.DEF_BUTLAST"
obua@17644	2117	"DEF_BOTTOM" > "HOLLight.hollight.DEF_BOTTOM"
kaliszyk@44639	2118	"DEF_BIT1" > "HOLLightCompat.BIT1_DEF"
kaliszyk@44639	2119	"DEF_BIT0" > "HOLLightCompat.BIT0_DEF"
obua@17644	2120	"DEF_BIJ" > "HOLLight.hollight.DEF_BIJ"
kaliszyk@44639	2121	"DEF_ASCII" > "HOLLight.hollight.DEF_ASCII"
kaliszyk@44639	2122	"DEF_APPEND" > "HOLLightList.DEF_APPEND"
kaliszyk@44639	2123	"DEF_ALL2" > "HOLLightList.DEF_ALL2"
kaliszyk@44639	2124	"DEF_ALL" > "HOLLightList.DEF_ALL"
kaliszyk@44639	2125	"DEF_-" > "HOLLightCompat.DEF_MINUS"
kaliszyk@44639	2126	"DEF_+" > "HOLLightCompat.DEF_PLUS"
obua@17644	2127	"DEF_$" > "HOLLight.hollight.DEF_$"
obua@17644	2128	"DECOMPOSITION" > "HOLLight.hollight.DECOMPOSITION"
obua@17644	2129	"DECIMAL_def" > "HOLLight.hollight.DECIMAL_def"
kaliszyk@44639	2130	"CROSS_def" > "HOLLight.hollight.CROSS_def"
kaliszyk@44639	2131	"CROSS_EQ_EMPTY" > "HOLLight.hollight.CROSS_EQ_EMPTY"
obua@17644	2132	"COUNTABLE_def" > "HOLLight.hollight.COUNTABLE_def"
kaliszyk@44639	2133	"CONS_HD_TL" > "List.hd_Cons_tl"
kaliszyk@44639	2134	"CONS_11" > "List.list.inject"
obua@17644	2135	"CONSTR_def" > "HOLLight.hollight.CONSTR_def"
obua@17644	2136	"CONSTR_REC" > "HOLLight.hollight.CONSTR_REC"
obua@17644	2137	"CONSTR_INJ" > "HOLLight.hollight.CONSTR_INJ"
obua@17644	2138	"CONSTR_IND" > "HOLLight.hollight.CONSTR_IND"
obua@17644	2139	"CONSTR_BOT" > "HOLLight.hollight.CONSTR_BOT"
kaliszyk@44639	2140	"CONJ_SYM" > "Groebner_Basis.dnf_3"
kaliszyk@44639	2141	"CONJ_ASSOC" > "HOL.conj_ac_3"
obua@17644	2142	"CONJ_ACI" > "HOLLight.hollight.CONJ_ACI"
obua@17644	2143	"COND_RATOR" > "HOLLight.hollight.COND_RATOR"
kaliszyk@44639	2144	"COND_RAND" > "HOL.if_distrib"
kaliszyk@44639	2145	"COND_ID" > "HOL.if_cancel"
obua@17644	2146	"COND_EXPAND" > "HOLLight.hollight.COND_EXPAND"
obua@17644	2147	"COND_EQ_CLAUSE" > "HOLLight.hollight.COND_EQ_CLAUSE"
kaliszyk@44639	2148	"COND_ELIM_THM" > "HOL.if_splits_1"
obua@17644	2149	"COND_CLAUSES" > "HOLLight.hollight.COND_CLAUSES"
obua@17644	2150	"COND_ABS" > "HOLLight.hollight.COND_ABS"
kaliszyk@44639	2151	"COMPONENT" > "Set.insertI1"
kaliszyk@44639	2152	"CHOOSE_SUBSET_STRONG" > "HOLLight.hollight.CHOOSE_SUBSET_STRONG"
obua@17644	2153	"CHOOSE_SUBSET" > "HOLLight.hollight.CHOOSE_SUBSET"
obua@17644	2154	"CHOICE_DEF" > "HOLLight.hollight.CHOICE_DEF"
obua@17644	2155	"CASEWISE_def" > "HOLLight.hollight.CASEWISE_def"
kaliszyk@44639	2156	"CART_EQ_FULL" > "HOLLight.hollight.CART_EQ_FULL"
obua@17644	2157	"CART_EQ" > "HOLLight.hollight.CART_EQ"
obua@17644	2158	"CARD_def" > "HOLLight.hollight.CARD_def"
kaliszyk@44639	2159	"CARD_UNION_OVERLAP_EQ" > "HOLLight.hollight.CARD_UNION_OVERLAP_EQ"
kaliszyk@44639	2160	"CARD_UNION_OVERLAP" > "HOLLight.hollight.CARD_UNION_OVERLAP"
obua@17644	2161	"CARD_UNION_LE" > "HOLLight.hollight.CARD_UNION_LE"
kaliszyk@44639	2162	"CARD_UNION_GEN" > "HOLLight.hollight.CARD_UNION_GEN"
obua@17644	2163	"CARD_UNION_EQ" > "HOLLight.hollight.CARD_UNION_EQ"
obua@17644	2164	"CARD_UNIONS_LE" > "HOLLight.hollight.CARD_UNIONS_LE"
kaliszyk@44639	2165	"CARD_UNIONS" > "HOLLight.hollight.CARD_UNIONS"
obua@17644	2166	"CARD_UNION" > "HOLLight.hollight.CARD_UNION"
obua@17644	2167	"CARD_SUBSET_LE" > "HOLLight.hollight.CARD_SUBSET_LE"
kaliszyk@44639	2168	"CARD_SUBSET_IMAGE" > "HOLLight.hollight.CARD_SUBSET_IMAGE"
obua@17644	2169	"CARD_SUBSET_EQ" > "HOLLight.hollight.CARD_SUBSET_EQ"
obua@17644	2170	"CARD_SUBSET" > "HOLLight.hollight.CARD_SUBSET"
obua@17644	2171	"CARD_PSUBSET" > "HOLLight.hollight.CARD_PSUBSET"
obua@17644	2172	"CARD_PRODUCT" > "HOLLight.hollight.CARD_PRODUCT"
obua@17644	2173	"CARD_POWERSET" > "HOLLight.hollight.CARD_POWERSET"
obua@17644	2174	"CARD_NUMSEG_LT" > "HOLLight.hollight.CARD_NUMSEG_LT"
obua@17644	2175	"CARD_NUMSEG_LEMMA" > "HOLLight.hollight.CARD_NUMSEG_LEMMA"
obua@17644	2176	"CARD_NUMSEG_LE" > "HOLLight.hollight.CARD_NUMSEG_LE"
obua@17644	2177	"CARD_NUMSEG_1" > "HOLLight.hollight.CARD_NUMSEG_1"
obua@17644	2178	"CARD_NUMSEG" > "HOLLight.hollight.CARD_NUMSEG"
obua@17644	2179	"CARD_LE_INJ" > "HOLLight.hollight.CARD_LE_INJ"
obua@17644	2180	"CARD_IMAGE_LE" > "HOLLight.hollight.CARD_IMAGE_LE"
kaliszyk@44639	2181	"CARD_IMAGE_INJ_EQ" > "HOLLight.hollight.CARD_IMAGE_INJ_EQ"
obua@17644	2182	"CARD_IMAGE_INJ" > "HOLLight.hollight.CARD_IMAGE_INJ"
obua@17644	2183	"CARD_FUNSPACE" > "HOLLight.hollight.CARD_FUNSPACE"
obua@17644	2184	"CARD_FINITE_IMAGE" > "HOLLight.hollight.CARD_FINITE_IMAGE"
obua@17644	2185	"CARD_EQ_SUM" > "HOLLight.hollight.CARD_EQ_SUM"
obua@17644	2186	"CARD_EQ_NSUM" > "HOLLight.hollight.CARD_EQ_NSUM"
kaliszyk@44639	2187	"CARD_EQ_BIJECTIONS" > "HOLLight.hollight.CARD_EQ_BIJECTIONS"
kaliszyk@44639	2188	"CARD_EQ_BIJECTION" > "HOLLight.hollight.CARD_EQ_BIJECTION"
obua@17644	2189	"CARD_EQ_0" > "HOLLight.hollight.CARD_EQ_0"
kaliszyk@44639	2190	"CARD_DIFF" > "HOLLight.hollight.CARD_DIFF"
obua@17644	2191	"CARD_DELETE" > "HOLLight.hollight.CARD_DELETE"
kaliszyk@44639	2192	"CARD_CROSS" > "HOLLight.hollight.CARD_CROSS"
obua@17644	2193	"CARD_CLAUSES" > "HOLLight.hollight.CARD_CLAUSES"
obua@17644	2194	"BOUNDS_NOTZERO" > "HOLLight.hollight.BOUNDS_NOTZERO"
obua@17644	2195	"BOUNDS_LINEAR_0" > "HOLLight.hollight.BOUNDS_LINEAR_0"
obua@17644	2196	"BOUNDS_LINEAR" > "HOLLight.hollight.BOUNDS_LINEAR"
obua@17644	2197	"BOUNDS_IGNORE" > "HOLLight.hollight.BOUNDS_IGNORE"
obua@17644	2198	"BOUNDS_DIVIDED" > "HOLLight.hollight.BOUNDS_DIVIDED"
obua@17644	2199	"BOTTOM_def" > "HOLLight.hollight.BOTTOM_def"
kaliszyk@44639	2200	"BOOL_CASES_AX" > "HOL.True_or_False"
kaliszyk@44639	2201	"BIT1_THM" > "HOLLight.hollight.BIT1_THM"
kaliszyk@44639	2202	"BIT1" > "HOLLight.hollight.BIT1"
kaliszyk@44639	2203	"BIT0_THM" > "Int.semiring_mult_2"
kaliszyk@44639	2204	"BIT0" > "Int.semiring_mult_2"
obua@17644	2205	"BIJ_def" > "HOLLight.hollight.BIJ_def"
kaliszyk@44639	2206	"BIJECTIVE_ON_LEFT_RIGHT_INVERSE" > "HOLLight.hollight.BIJECTIVE_ON_LEFT_RIGHT_INVERSE"
kaliszyk@44639	2207	"BIJECTIVE_LEFT_RIGHT_INVERSE" > "HOLLight.hollight.BIJECTIVE_LEFT_RIGHT_INVERSE"
kaliszyk@44639	2208	"BIJECTIONS_HAS_SIZE_EQ" > "HOLLight.hollight.BIJECTIONS_HAS_SIZE_EQ"
kaliszyk@44639	2209	"BIJECTIONS_HAS_SIZE" > "HOLLight.hollight.BIJECTIONS_HAS_SIZE"
kaliszyk@44639	2210	"BIJECTIONS_CARD_EQ" > "HOLLight.hollight.BIJECTIONS_CARD_EQ"
kaliszyk@44639	2211	"BETA_THM" > "HOL.eta_contract_eq"
kaliszyk@44639	2212	"ASCII_def" > "HOLLight.hollight.ASCII_def"
obua@17644	2213	"ARITH_ZERO" > "HOLLight.hollight.ARITH_ZERO"
obua@17644	2214	"ARITH_SUC" > "HOLLight.hollight.ARITH_SUC"
obua@17644	2215	"ARITH_SUB" > "HOLLight.hollight.ARITH_SUB"
obua@17644	2216	"ARITH_PRE" > "HOLLight.hollight.ARITH_PRE"
obua@17644	2217	"ARITH_ODD" > "HOLLight.hollight.ARITH_ODD"
obua@17644	2218	"ARITH_MULT" > "HOLLight.hollight.ARITH_MULT"
obua@17644	2219	"ARITH_LT" > "HOLLight.hollight.ARITH_LT"
obua@17644	2220	"ARITH_LE" > "HOLLight.hollight.ARITH_LE"
obua@17644	2221	"ARITH_EXP" > "HOLLight.hollight.ARITH_EXP"
obua@17644	2222	"ARITH_EVEN" > "HOLLight.hollight.ARITH_EVEN"
obua@17644	2223	"ARITH_EQ" > "HOLLight.hollight.ARITH_EQ"
obua@17644	2224	"ARITH_ADD" > "HOLLight.hollight.ARITH_ADD"
kaliszyk@44639	2225	"APPEND_NIL" > "List.append_Nil2"
kaliszyk@44639	2226	"APPEND_EQ_NIL" > "List.append_is_Nil_conv"
kaliszyk@44639	2227	"APPEND_BUTLAST_LAST" > "List.append_butlast_last_id"
kaliszyk@44639	2228	"APPEND_ASSOC" > "List.append_assoc"
obua@17644	2229	"AND_FORALL_THM" > "HOL.all_conj_distrib"
obua@17644	2230	"AND_CLAUSES" > "HOLLight.hollight.AND_CLAUSES"
kaliszyk@44639	2231	"AND_ALL2" > "HOLLightList.AND_ALL2"
kaliszyk@44639	2232	"AND_ALL" > "HOLLightList.AND_ALL"
kaliszyk@44639	2233	"ALL_T" > "HOLLightList.ALL_T"
kaliszyk@44639	2234	"ALL_MP" > "HOLLightList.ALL_MP"
kaliszyk@44639	2235	"ALL_MEM" > "HOLLightList.ALL_MEM"
kaliszyk@44639	2236	"ALL_IMP" > "HOLLightList.ALL_IMP"
kaliszyk@44639	2237	"ALL_EL" > "List.list_all_length"
kaliszyk@44639	2238	"ALL_APPEND" > "List.list_all_append"
kaliszyk@44639	2239	"ALL2_MAP2" > "HOLLightList.ALL2_MAP2"
kaliszyk@44639	2240	"ALL2_MAP" > "HOLLightList.ALL2_MAP"
kaliszyk@44639	2241	"ALL2_AND_RIGHT" > "HOLLightList.ALL2_AND_RIGHT"
kaliszyk@44639	2242	"ALL2_ALL" > "HOLLightList.ALL2_ALL"
kaliszyk@44639	2243	"ALL2" > "HOLLightList.ALL2"
kaliszyk@44639	2244	"ADMISSIBLE_UNGUARDED_PATTERN" > "HOLLight.hollight.ADMISSIBLE_UNGUARDED_PATTERN"
obua@19093	2245	"ADMISSIBLE_SUM" > "HOLLight.hollight.ADMISSIBLE_SUM"
kaliszyk@44639	2246	"ADMISSIBLE_SEQPATTERN" > "HOLLight.hollight.ADMISSIBLE_SEQPATTERN"
kaliszyk@44639	2247	"ADMISSIBLE_RAND" > "HOLLight.hollight.ADMISSIBLE_RAND"
obua@19093	2248	"ADMISSIBLE_NSUM" > "HOLLight.hollight.ADMISSIBLE_NSUM"
obua@17644	2249	"ADMISSIBLE_NEST" > "HOLLight.hollight.ADMISSIBLE_NEST"
kaliszyk@44639	2250	"ADMISSIBLE_MATCH_SEQPATTERN" > "HOLLight.hollight.ADMISSIBLE_MATCH_SEQPATTERN"
kaliszyk@44639	2251	"ADMISSIBLE_MATCH" > "HOLLight.hollight.ADMISSIBLE_MATCH"
kaliszyk@44639	2252	"ADMISSIBLE_MAP" > "HOLLight.hollight.ADMISSIBLE_MAP"
obua@17644	2253	"ADMISSIBLE_LAMBDA" > "HOLLight.hollight.ADMISSIBLE_LAMBDA"
obua@17644	2254	"ADMISSIBLE_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.ADMISSIBLE_IMP_SUPERADMISSIBLE"
kaliszyk@44639	2255	"ADMISSIBLE_GUARDED_PATTERN" > "HOLLight.hollight.ADMISSIBLE_GUARDED_PATTERN"
obua@17644	2256	"ADMISSIBLE_CONST" > "HOLLight.hollight.ADMISSIBLE_CONST"
obua@17644	2257	"ADMISSIBLE_COND" > "HOLLight.hollight.ADMISSIBLE_COND"
obua@17644	2258	"ADMISSIBLE_COMB" > "HOLLight.hollight.ADMISSIBLE_COMB"
obua@17644	2259	"ADMISSIBLE_BASE" > "HOLLight.hollight.ADMISSIBLE_BASE"
kaliszyk@44639	2260	"ADD_SYM" > "Fields.linordered_field_class.sign_simps_43"
obua@17644	2261	"ADD_SUC" > "Nat.add_Suc_right"
obua@17644	2262	"ADD_SUBR2" > "Nat.diff_add_0"
obua@17644	2263	"ADD_SUBR" > "HOLLight.hollight.ADD_SUBR"
obua@17644	2264	"ADD_SUB2" > "Nat.diff_add_inverse"
obua@17644	2265	"ADD_SUB" > "Nat.diff_add_inverse2"
obua@17644	2266	"ADD_EQ_0" > "Nat.add_is_0"
obua@17644	2267	"ADD_CLAUSES" > "HOLLight.hollight.ADD_CLAUSES"
kaliszyk@44639	2268	"ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_44"
obua@17644	2269	"ADD_AC" > "HOLLight.hollight.ADD_AC"
kaliszyk@44639	2270	"ADD_0" > "Divides.arithmetic_simps_39"
kaliszyk@44639	2271	"ADD1" > "Nat_Numeral.Suc_eq_plus1"
kaliszyk@44639	2272	"ABS_SIMP" > "HOL.refl"
obua@17644	2273	"ABSORPTION" > "HOLLight.hollight.ABSORPTION"
kaliszyk@44639	2274	">_c_def" > "HOLLight.hollight.>_c_def"
kaliszyk@44639	2275	">=_c_def" > "HOLLight.hollight.>=_c_def"
kaliszyk@44639	2276	"=_c_def" > "HOLLight.hollight.=_c_def"
kaliszyk@44639	2277	"<_c_def" > "HOLLight.hollight.<_c_def"
kaliszyk@44639	2278	"<=_c_def" > "HOLLight.hollight.<=_c_def"
obua@17644	2279	"$_def" > "HOLLight.hollight.$_def"
obua@17644	2280
obua@17644	2281	ignore_thms
kaliszyk@44714	2282	"WF_REC_CASES"
obua@19093	2283	"TYDEF_sum"
obua@17644	2284	"TYDEF_prod"
kaliszyk@44639	2285	"TYDEF_option"
obua@17644	2286	"TYDEF_num"
kaliszyk@44639	2287	"TYDEF_list"
obua@17644	2288	"TYDEF_1"
kaliszyk@44639	2289	"SNDCART_PASTECART"
kaliszyk@44639	2290	"SET_OF_LIST_OF_SET"
kaliszyk@44639	2291	"REP_ABS_PAIR"
kaliszyk@44714	2292	"RECURSION_CASEWISE_PAIRWISE"
kaliszyk@44714	2293	"RECURSION_CASEWISE"
kaliszyk@44639	2294	"PASTECART_FST_SND"
kaliszyk@44639	2295	"PASTECART_EQ"
kaliszyk@44639	2296	"MEM_LIST_OF_SET"
kaliszyk@44639	2297	"MEM_ASSOC"
kaliszyk@44639	2298	"LIST_OF_SET_PROPERTIES"
kaliszyk@44639	2299	"LENGTH_LIST_OF_SET"
kaliszyk@44714	2300	"HAS_SIZE_SET_OF_LIST"
kaliszyk@44639	2301	"FSTCART_PASTECART"
kaliszyk@44639	2302	"FORALL_PASTECART"
kaliszyk@44639	2303	"FINITE_SET_OF_LIST"
kaliszyk@44639	2304	"EX_MAP"
kaliszyk@44639	2305	"EXISTS_PASTECART"
kaliszyk@44639	2306	"EL_TL"
kaliszyk@44639	2307	"DIMINDEX_HAS_SIZE_FINITE_SUM"
kaliszyk@44639	2308	"DIMINDEX_FINITE_SUM"
obua@17644	2309	"DEF_one"
kaliszyk@44639	2310	"DEF_mk_pair"
kaliszyk@44639	2311	"DEF_list_of_set"
obua@17644	2312	"DEF__0"
kaliszyk@44639	2313	"DEF_ZIP"
kaliszyk@44639	2314	"DEF_TL"
obua@17644	2315	"DEF_SUC"
kaliszyk@44639	2316	"DEF_SOME"
kaliszyk@44639	2317	"DEF_OUTR"
kaliszyk@44639	2318	"DEF_OUTL"
kaliszyk@44639	2319	"DEF_NONE"
kaliszyk@44639	2320	"DEF_NIL"
kaliszyk@44639	2321	"DEF_MAP2"
kaliszyk@44639	2322	"DEF_ITLIST2"
obua@19093	2323	"DEF_INR"
obua@19093	2324	"DEF_INL"
kaliszyk@44639	2325	"DEF_HD"
kaliszyk@44639	2326	"DEF_CONS"
kaliszyk@44639	2327	"DEF_ASSOC"
kaliszyk@44639	2328	"DEF_,"
kaliszyk@44714	2329	"CASEWISE_WORKS"
kaliszyk@44714	2330	"CASEWISE_CASES"
kaliszyk@44714	2331	"CASEWISE"
kaliszyk@44714	2332	"CARD_SET_OF_LIST_LE"
kaliszyk@44639	2333	"ALL_MAP"
obua@17644	2334
obua@17644	2335	end

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Wed, 20 Jul 2011 10:11:08 +0200
changeset 44789	6ca79a354c51
parent 44714	16f2fd9103bd
child 44953	81e55342cb86
permissions	-rw-r--r--