import
import_segment "hollight"
def_maps
"vector" > "vector_def"
"treal_of_num" > "treal_of_num_def"
"treal_neg" > "treal_neg_def"
"treal_mul" > "treal_mul_def"
"treal_le" > "treal_le_def"
"treal_inv" > "treal_inv_def"
"treal_eq" > "treal_eq_def"
"treal_add" > "treal_add_def"
"tailadmissible" > "tailadmissible_def"
"support" > "support_def"
"superadmissible" > "superadmissible_def"
"sum" > "sum_def"
"sndcart" > "sndcart_def"
"rem" > "rem_def"
"real_sub" > "real_sub_def"
"real_sgn" > "real_sgn_def"
"real_pow" > "real_pow_def"
"real_of_num" > "real_of_num_def"
"real_neg" > "real_neg_def"
"real_mul" > "real_mul_def"
"real_mod" > "real_mod_def"
"real_min" > "real_min_def"
"real_max" > "real_max_def"
"real_lt" > "real_lt_def"
"real_le" > "real_le_def"
"real_inv" > "real_inv_def"
"real_gt" > "real_gt_def"
"real_ge" > "real_ge_def"
"real_div" > "real_div_def"
"real_add" > "real_add_def"
"real_abs" > "real_abs_def"
"pastecart" > "pastecart_def"
"pairwise" > "pairwise_def"
"num_of_int" > "num_of_int_def"
"num_mod" > "num_mod_def"
"num_gcd" > "num_gcd_def"
"num_divides" > "num_divides_def"
"num_coprime" > "num_coprime_def"
"nsum" > "nsum_def"
"neutral" > "neutral_def"
"nadd_rinv" > "nadd_rinv_def"
"nadd_of_num" > "nadd_of_num_def"
"nadd_mul" > "nadd_mul_def"
"nadd_le" > "nadd_le_def"
"nadd_inv" > "nadd_inv_def"
"nadd_eq" > "nadd_eq_def"
"nadd_add" > "nadd_add_def"
"monoidal" > "monoidal_def"
"minimal" > "minimal_def"
"lambda" > "lambda_def"
"iterate" > "iterate_def"
"is_nadd" > "is_nadd_def"
"integer" > "integer_def"
"int_sub" > "int_sub_def"
"int_sgn" > "int_sgn_def"
"int_pow" > "int_pow_def"
"int_of_num" > "int_of_num_def"
"int_neg" > "int_neg_def"
"int_mul" > "int_mul_def"
"int_mod" > "int_mod_def"
"int_min" > "int_min_def"
"int_max" > "int_max_def"
"int_lt" > "int_lt_def"
"int_le" > "int_le_def"
"int_gt" > "int_gt_def"
"int_ge" > "int_ge_def"
"int_gcd" > "int_gcd_def"
"int_divides" > "int_divides_def"
"int_coprime" > "int_coprime_def"
"int_add" > "int_add_def"
"int_abs" > "int_abs_def"
"hreal_of_num" > "hreal_of_num_def"
"hreal_mul" > "hreal_mul_def"
"hreal_le" > "hreal_le_def"
"hreal_inv" > "hreal_inv_def"
"hreal_add" > "hreal_add_def"
"fstcart" > "fstcart_def"
"eqeq" > "eqeq_def"
"div" > "div_def"
"dist" > "dist_def"
"dimindex" > "dimindex_def"
"admissible" > "admissible_def"
"_UNGUARDED_PATTERN" > "_UNGUARDED_PATTERN_def"
"_SEQPATTERN" > "_SEQPATTERN_def"
"_MATCH" > "_MATCH_def"
"_GUARDED_PATTERN" > "_GUARDED_PATTERN_def"
"_FUNCTION" > "_FUNCTION_def"
"_FALSITY_" > "_FALSITY__def"
"_11937" > "_11937_def"
"ZRECSPACE" > "ZRECSPACE_def"
"ZCONSTR" > "ZCONSTR_def"
"ZBOT" > "ZBOT_def"
"UNCURRY" > "UNCURRY_def"
"SURJ" > "SURJ_def"
"SING" > "SING_def"
"REST" > "REST_def"
"PASSOC" > "PASSOC_def"
"PAIRWISE" > "PAIRWISE_def"
"NUM_REP" > "NUM_REP_def"
"NUMSUM" > "NUMSUM_def"
"NUMSND" > "NUMSND_def"
"NUMRIGHT" > "NUMRIGHT_def"
"NUMPAIR" > "NUMPAIR_def"
"NUMLEFT" > "NUMLEFT_def"
"NUMFST" > "NUMFST_def"
"LET_END" > "LET_END_def"
"ITSET" > "ITSET_def"
"ISO" > "ISO_def"
"INJP" > "INJP_def"
"INJN" > "INJN_def"
"INJF" > "INJF_def"
"INJA" > "INJA_def"
"INJ" > "INJ_def"
"IND_SUC" > "IND_SUC_def"
"IND_0" > "IND_0_def"
"HAS_SIZE" > "HAS_SIZE_def"
"FNIL" > "FNIL_def"
"FINREC" > "FINREC_def"
"FCONS" > "FCONS_def"
"DECIMAL" > "DECIMAL_def"
"CROSS" > "CROSS_def"
"COUNTABLE" > "COUNTABLE_def"
"CONSTR" > "CONSTR_def"
"CASEWISE" > "CASEWISE_def"
"CARD" > "CARD_def"
"BOTTOM" > "BOTTOM_def"
"BIJ" > "BIJ_def"
"ASCII" > "ASCII_def"
">_c" > ">_c_def"
">=_c" > ">=_c_def"
"=_c" > "=_c_def"
"<_c" > "<_c_def"
"<=_c" > "<=_c_def"
"$" > "$_def"
type_maps
"sum" > "Sum_Type.sum"
"recspace" > "HOLLight.hollight.recspace"
"real" > "HOLLight.hollight.real"
"prod" > "Product_Type.prod"
"option" > "Datatype.option"
"num" > "Nat.nat"
"nadd" > "HOLLight.hollight.nadd"
"list" > "List.list"
"int" > "HOLLight.hollight.int"
"ind" > "Nat.ind"
"hreal" > "HOLLight.hollight.hreal"
"fun" > "fun"
"finite_sum" > "HOLLight.hollight.finite_sum"
"finite_image" > "HOLLight.hollight.finite_image"
"char" > "HOLLight.hollight.char"
"cart" > "HOLLight.hollight.cart"
"bool" > "HOL.bool"
"N_3" > "HOLLight.hollight.N_3"
"N_2" > "HOLLight.hollight.N_2"
"N_1" > "Product_Type.unit"
const_maps
"~" > "HOL.Not"
"vector" > "HOLLight.hollight.vector"
"treal_of_num" > "HOLLight.hollight.treal_of_num"
"treal_neg" > "HOLLight.hollight.treal_neg"
"treal_mul" > "HOLLight.hollight.treal_mul"
"treal_le" > "HOLLight.hollight.treal_le"
"treal_inv" > "HOLLight.hollight.treal_inv"
"treal_eq" > "HOLLight.hollight.treal_eq"
"treal_add" > "HOLLight.hollight.treal_add"
"tailadmissible" > "HOLLight.hollight.tailadmissible"
"support" > "HOLLight.hollight.support"
"superadmissible" > "HOLLight.hollight.superadmissible"
"sum" > "HOLLight.hollight.sum"
"sndcart" > "HOLLight.hollight.sndcart"
"set_of_list" > "List.set"
"rem" > "HOLLight.hollight.rem"
"real_sub" > "HOLLight.hollight.real_sub"
"real_sgn" > "HOLLight.hollight.real_sgn"
"real_pow" > "HOLLight.hollight.real_pow"
"real_of_num" > "HOLLight.hollight.real_of_num"
"real_neg" > "HOLLight.hollight.real_neg"
"real_mul" > "HOLLight.hollight.real_mul"
"real_mod" > "HOLLight.hollight.real_mod"
"real_min" > "HOLLight.hollight.real_min"
"real_max" > "HOLLight.hollight.real_max"
"real_lt" > "HOLLight.hollight.real_lt"
"real_le" > "HOLLight.hollight.real_le"
"real_inv" > "HOLLight.hollight.real_inv"
"real_gt" > "HOLLight.hollight.real_gt"
"real_ge" > "HOLLight.hollight.real_ge"
"real_div" > "HOLLight.hollight.real_div"
"real_add" > "HOLLight.hollight.real_add"
"real_abs" > "HOLLight.hollight.real_abs"
"pastecart" > "HOLLight.hollight.pastecart"
"pairwise" > "HOLLight.hollight.pairwise"
"one" > "Product_Type.Unity"
"o" > "Fun.comp"
"num_of_int" > "HOLLight.hollight.num_of_int"
"num_mod" > "HOLLight.hollight.num_mod"
"num_gcd" > "HOLLight.hollight.num_gcd"
"num_divides" > "HOLLight.hollight.num_divides"
"num_coprime" > "HOLLight.hollight.num_coprime"
"nsum" > "HOLLight.hollight.nsum"
"neutral" > "HOLLight.hollight.neutral"
"nadd_rinv" > "HOLLight.hollight.nadd_rinv"
"nadd_of_num" > "HOLLight.hollight.nadd_of_num"
"nadd_mul" > "HOLLight.hollight.nadd_mul"
"nadd_le" > "HOLLight.hollight.nadd_le"
"nadd_inv" > "HOLLight.hollight.nadd_inv"
"nadd_eq" > "HOLLight.hollight.nadd_eq"
"nadd_add" > "HOLLight.hollight.nadd_add"
"monoidal" > "HOLLight.hollight.monoidal"
"mk_pair" > "Product_Type.Pair_Rep"
"mk_num" > "Fun.id"
"minimal" > "HOLLight.hollight.minimal"
"list_EX" > "List.list_ex"
"list_ALL" > "List.list_all"
"lambda" > "HOLLight.hollight.lambda"
"iterate" > "HOLLight.hollight.iterate"
"is_nadd" > "HOLLight.hollight.is_nadd"
"integer" > "HOLLight.hollight.integer"
"int_sub" > "HOLLight.hollight.int_sub"
"int_sgn" > "HOLLight.hollight.int_sgn"
"int_pow" > "HOLLight.hollight.int_pow"
"int_of_num" > "HOLLight.hollight.int_of_num"
"int_neg" > "HOLLight.hollight.int_neg"
"int_mul" > "HOLLight.hollight.int_mul"
"int_mod" > "HOLLight.hollight.int_mod"
"int_min" > "HOLLight.hollight.int_min"
"int_max" > "HOLLight.hollight.int_max"
"int_lt" > "HOLLight.hollight.int_lt"
"int_le" > "HOLLight.hollight.int_le"
"int_gt" > "HOLLight.hollight.int_gt"
"int_ge" > "HOLLight.hollight.int_ge"
"int_gcd" > "HOLLight.hollight.int_gcd"
"int_divides" > "HOLLight.hollight.int_divides"
"int_coprime" > "HOLLight.hollight.int_coprime"
"int_add" > "HOLLight.hollight.int_add"
"int_abs" > "HOLLight.hollight.int_abs"
"hreal_of_num" > "HOLLight.hollight.hreal_of_num"
"hreal_mul" > "HOLLight.hollight.hreal_mul"
"hreal_le" > "HOLLight.hollight.hreal_le"
"hreal_inv" > "HOLLight.hollight.hreal_inv"
"hreal_add" > "HOLLight.hollight.hreal_add"
"fstcart" > "HOLLight.hollight.fstcart"
"eqeq" > "HOLLight.hollight.eqeq"
"div" > "HOLLight.hollight.div"
"dist" > "HOLLight.hollight.dist"
"dimindex" > "HOLLight.hollight.dimindex"
"admissible" > "HOLLight.hollight.admissible"
"_UNGUARDED_PATTERN" > "HOLLight.hollight._UNGUARDED_PATTERN"
"_SEQPATTERN" > "HOLLight.hollight._SEQPATTERN"
"_MATCH" > "HOLLight.hollight._MATCH"
"_GUARDED_PATTERN" > "HOLLight.hollight._GUARDED_PATTERN"
"_FUNCTION" > "HOLLight.hollight._FUNCTION"
"_FALSITY_" > "HOLLight.hollight._FALSITY_"
"_11937" > "HOLLight.hollight._11937"
"_0" > "Groups.zero_class.zero" :: "nat"
"\\/" > "HOL.disj"
"ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
"ZIP" > "List.zip"
"ZCONSTR" > "HOLLight.hollight.ZCONSTR"
"ZBOT" > "HOLLight.hollight.ZBOT"
"WF" > "Wellfounded.wfP"
"UNIV" > "Orderings.top_class.top" :: "'a => bool"
"UNIONS" > "Complete_Lattices.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
"UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
"UNCURRY" > "HOLLight.hollight.UNCURRY"
"TL" > "List.tl"
"T" > "HOL.True"
"SURJ" > "HOLLight.hollight.SURJ"
"SUC" > "Nat.Suc"
"SUBSET" > "Orderings.ord_class.less_eq" :: "('a => bool) => ('a => bool) => bool"
"SOME" > "Datatype.Some"
"SND" > "Product_Type.snd"
"SING" > "HOLLight.hollight.SING"
"SETSPEC" > "HOLLightCompat.SETSPEC"
"REVERSE" > "List.rev"
"REST" > "HOLLight.hollight.REST"
"REPLICATE" > "List.replicate"
"PSUBSET" > "Orderings.ord_class.less" :: "('a => bool) => ('a => bool) => bool"
"PRE" > "HOLLightCompat.Pred"
"PASSOC" > "HOLLight.hollight.PASSOC"
"PAIRWISE" > "HOLLight.hollight.PAIRWISE"
"OUTR" > "HOLLightCompat.OUTR"
"OUTL" > "HOLLightCompat.OUTL"
"ONTO" > "Fun.surj"
"ONE_ONE" > "Fun.inj"
"ODD" > "HOLLightCompat.ODD"
"NUM_REP" > "HOLLight.hollight.NUM_REP"
"NUMSUM" > "HOLLight.hollight.NUMSUM"
"NUMSND" > "HOLLight.hollight.NUMSND"
"NUMRIGHT" > "HOLLight.hollight.NUMRIGHT"
"NUMPAIR" > "HOLLight.hollight.NUMPAIR"
"NUMLEFT" > "HOLLight.hollight.NUMLEFT"
"NUMFST" > "HOLLight.hollight.NUMFST"
"NUMERAL" > "HOLLightCompat.NUMERAL"
"NULL" > "List.null"
"NONE" > "Datatype.None"
"NIL" > "List.list.Nil"
"MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
"MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
"MEM" > "HOLLightList.list_mem"
"MEASURE" > "HOLLightCompat.MEASURE"
"MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
"MAP2" > "HOLLightList.map2"
"MAP" > "List.map"
"LET_END" > "HOLLight.hollight.LET_END"
"LET" > "HOLLightCompat.LET"
"LENGTH" > "List.length"
"LAST" > "List.last"
"ITSET" > "HOLLight.hollight.ITSET"
"ITLIST2" > "HOLLightList.fold2"
"ITLIST" > "List.foldr"
"ISO" > "HOLLight.hollight.ISO"
"INTERS" > "Complete_Lattices.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
"INTER" > "Lattices.inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
"INSERT" > "Set.insert"
"INR" > "Sum_Type.Inr"
"INL" > "Sum_Type.Inl"
"INJP" > "HOLLight.hollight.INJP"
"INJN" > "HOLLight.hollight.INJN"
"INJF" > "HOLLight.hollight.INJF"
"INJA" > "HOLLight.hollight.INJA"
"INJ" > "HOLLight.hollight.INJ"
"INFINITE" > "HOLLightCompat.INFINITE"
"IND_SUC" > "HOLLight.hollight.IND_SUC"
"IND_0" > "HOLLight.hollight.IND_0"
"IN" > "Set.member"
"IMAGE" > "Set.image"
"I" > "Fun.id"
"HD" > "List.hd"
"HAS_SIZE" > "HOLLight.hollight.HAS_SIZE"
"GSPEC" > "Set.Collect"
"GEQ" > "HOL.eq"
"GABS" > "Hilbert_Choice.Eps"
"FST" > "Product_Type.fst"
"FNIL" > "HOLLight.hollight.FNIL"
"FINREC" > "HOLLight.hollight.FINREC"
"FINITE" > "Finite_Set.finite"
"FILTER" > "List.filter"
"FCONS" > "HOLLight.hollight.FCONS"
"FACT" > "Fact.fact_class.fact" :: "nat => nat"
"F" > "HOL.False"
"EXP" > "Power.power_class.power" :: "nat => nat => nat"
"EVEN" > "Parity.even_odd_class.even" :: "nat => bool"
"EMPTY" > "Orderings.bot_class.bot" :: "'a => bool"
"EL" > "HOLLightList.list_el"
"DIV" > "Divides.div_class.div" :: "nat => nat => nat"
"DISJOINT" > "HOLLightCompat.DISJOINT"
"DIFF" > "Groups.minus_class.minus" :: "('a => bool) => ('a => bool) => 'a => bool"
"DELETE" > "HOLLightCompat.DELETE"
"DECIMAL" > "HOLLight.hollight.DECIMAL"
"CURRY" > "Product_Type.curry"
"CROSS" > "HOLLight.hollight.CROSS"
"COUNTABLE" > "HOLLight.hollight.COUNTABLE"
"CONSTR" > "HOLLight.hollight.CONSTR"
"CONS" > "List.list.Cons"
"COND" > "HOL.If"
"CHOICE" > "Hilbert_Choice.Eps"
"CASEWISE" > "HOLLight.hollight.CASEWISE"
"CARD" > "HOLLight.hollight.CARD"
"BUTLAST" > "List.butlast"
"BOTTOM" > "HOLLight.hollight.BOTTOM"
"BIT1" > "HOLLightCompat.NUMERAL_BIT1"
"BIT0" > "HOLLightCompat.NUMERAL_BIT0"
"BIJ" > "HOLLight.hollight.BIJ"
"ASCII" > "HOLLight.hollight.ASCII"
"APPEND" > "List.append"
"ALL2" > "List.list_all2"
"@" > "Hilbert_Choice.Eps"
"?!" > "HOL.Ex1"
"?" > "HOL.Ex"
">_c" > "HOLLight.hollight.>_c"
">=_c" > "HOLLight.hollight.>=_c"
">=" > "Orderings.ord_class.greater_eq" :: "nat => nat => bool"
">" > "Orderings.ord_class.greater" :: "nat => nat => bool"
"=_c" > "HOLLight.hollight.=_c"
"==>" > "HOL.implies"
"=" > "HOL.eq"
"<_c" > "HOLLight.hollight.<_c"
"<=_c" > "HOLLight.hollight.<=_c"
"<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
"<" > "Orderings.ord_class.less" :: "nat => nat => bool"
"/\\" > "HOL.conj"
".." > "HOLLightCompat.dotdot"
"-" > "Groups.minus_class.minus" :: "nat => nat => nat"
"," > "Product_Type.Pair"
"+" > "Groups.plus_class.plus" :: "nat => nat => nat"
"*" > "Groups.times_class.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
"!" > "HOL.All"
const_renames
"EX" > "list_EX"
"ALL" > "list_ALL"
"==" > "eqeq"
thm_maps
"vector_def" > "HOLLight.hollight.vector_def"
"treal_of_num_def" > "HOLLight.hollight.treal_of_num_def"
"treal_neg_def" > "HOLLight.hollight.treal_neg_def"
"treal_mul_def" > "HOLLight.hollight.treal_mul_def"
"treal_le_def" > "HOLLight.hollight.treal_le_def"
"treal_inv_def" > "HOLLight.hollight.treal_inv_def"
"treal_eq_def" > "HOLLight.hollight.treal_eq_def"
"treal_add_def" > "HOLLight.hollight.treal_add_def"
"th_cond" > "HOLLight.hollight.th_cond"
"th" > "HOL.eta_contract_eq"
"tailadmissible_def" > "HOLLight.hollight.tailadmissible_def"
"support_def" > "HOLLight.hollight.support_def"
"superadmissible_def" > "HOLLight.hollight.superadmissible_def"
"sum_def" > "HOLLight.hollight.sum_def"
"string_INFINITE" > "List.infinite_UNIV_listI"
"sth" > "HOLLight.hollight.sth"
"sndcart_def" > "HOLLight.hollight.sndcart_def"
"right_th" > "HOLLight.hollight.right_th"
"rem_def" > "HOLLight.hollight.rem_def"
"real_sub_def" > "HOLLight.hollight.real_sub_def"
"real_sgn_def" > "HOLLight.hollight.real_sgn_def"
"real_pow_def" > "HOLLight.hollight.real_pow_def"
"real_of_num_def" > "HOLLight.hollight.real_of_num_def"
"real_neg_def" > "HOLLight.hollight.real_neg_def"
"real_mul_def" > "HOLLight.hollight.real_mul_def"
"real_mod_def" > "HOLLight.hollight.real_mod_def"
"real_min_def" > "HOLLight.hollight.real_min_def"
"real_max_def" > "HOLLight.hollight.real_max_def"
"real_lt_def" > "HOLLight.hollight.real_lt_def"
"real_le_def" > "HOLLight.hollight.real_le_def"
"real_inv_def" > "HOLLight.hollight.real_inv_def"
"real_gt_def" > "HOLLight.hollight.real_gt_def"
"real_ge_def" > "HOLLight.hollight.real_ge_def"
"real_div_def" > "HOLLight.hollight.real_div_def"
"real_add_def" > "HOLLight.hollight.real_add_def"
"real_abs_def" > "HOLLight.hollight.real_abs_def"
"real_INFINITE" > "HOLLight.hollight.real_INFINITE"
"pastecart_def" > "HOLLight.hollight.pastecart_def"
"pairwise_def" > "HOLLight.hollight.pairwise_def"
"pair_RECURSION" > "HOLLight.hollight.pair_RECURSION"
"pair_INDUCT" > "Product_Type.prod.induct"
"one_axiom" > "HOLLight.hollight.one_axiom"
"one_RECURSION" > "HOLLight.hollight.one_RECURSION"
"one_INDUCT" > "Product_Type.unit.induct"
"one_Axiom" > "HOLLight.hollight.one_Axiom"
"one" > "HOLLightCompat.one"
"o_THM" > "Fun.comp_def"
"o_ASSOC" > "HOLLight.hollight.o_ASSOC"
"num_of_int_def" > "HOLLight.hollight.num_of_int_def"
"num_mod_def" > "HOLLight.hollight.num_mod_def"
"num_gcd_def" > "HOLLight.hollight.num_gcd_def"
"num_divides_def" > "HOLLight.hollight.num_divides_def"
"num_coprime_def" > "HOLLight.hollight.num_coprime_def"
"num_congruent" > "HOLLight.hollight.num_congruent"
"num_WOP" > "HOLLight.hollight.num_WOP"
"num_WF" > "Nat.nat_less_induct"
"num_RECURSION_STD" > "HOLLight.hollight.num_RECURSION_STD"
"num_MAX" > "HOLLight.hollight.num_MAX"
"num_INFINITE" > "Finite_Set.infinite_UNIV_char_0"
"num_INDUCTION" > "Fact.fact_nat.induct"
"num_FINITE_AVOID" > "HOLLight.hollight.num_FINITE_AVOID"
"num_FINITE" > "HOLLight.hollight.num_FINITE"
"num_CASES" > "Nat.nat.nchotomy"
"num_Axiom" > "HOLLightCompat.num_Axiom"
"nsum_def" > "HOLLight.hollight.nsum_def"
"neutral_def" > "HOLLight.hollight.neutral_def"
"nadd_rinv_def" > "HOLLight.hollight.nadd_rinv_def"
"nadd_of_num_def" > "HOLLight.hollight.nadd_of_num_def"
"nadd_mul_def" > "HOLLight.hollight.nadd_mul_def"
"nadd_le_def" > "HOLLight.hollight.nadd_le_def"
"nadd_inv_def" > "HOLLight.hollight.nadd_inv_def"
"nadd_eq_def" > "HOLLight.hollight.nadd_eq_def"
"nadd_add_def" > "HOLLight.hollight.nadd_add_def"
"monoidal_def" > "HOLLight.hollight.monoidal_def"
"minimal_def" > "HOLLight.hollight.minimal_def"
"list_INDUCT" > "List.list.induct"
"list_CASES" > "List.list.nchotomy"
"lambda_def" > "HOLLight.hollight.lambda_def"
"iterate_def" > "HOLLight.hollight.iterate_def"
"is_nadd_def" > "HOLLight.hollight.is_nadd_def"
"is_nadd_0" > "HOLLight.hollight.is_nadd_0"
"is_int" > "HOLLight.hollight.is_int"
"integer_def" > "HOLLight.hollight.integer_def"
"int_sub_th" > "HOLLight.hollight.int_sub_th"
"int_sub_def" > "HOLLight.hollight.int_sub_def"
"int_sgn_th" > "HOLLight.hollight.int_sgn_th"
"int_sgn_def" > "HOLLight.hollight.int_sgn_def"
"int_pow_th" > "HOLLight.hollight.int_pow_th"
"int_pow_def" > "HOLLight.hollight.int_pow_def"
"int_of_num_th" > "HOLLight.hollight.int_of_num_th"
"int_of_num_def" > "HOLLight.hollight.int_of_num_def"
"int_neg_th" > "HOLLight.hollight.int_neg_th"
"int_neg_def" > "HOLLight.hollight.int_neg_def"
"int_mul_th" > "HOLLight.hollight.int_mul_th"
"int_mul_def" > "HOLLight.hollight.int_mul_def"
"int_mod_def" > "HOLLight.hollight.int_mod_def"
"int_min_th" > "HOLLight.hollight.int_min_th"
"int_min_def" > "HOLLight.hollight.int_min_def"
"int_max_th" > "HOLLight.hollight.int_max_th"
"int_max_def" > "HOLLight.hollight.int_max_def"
"int_lt_def" > "HOLLight.hollight.int_lt_def"
"int_le_def" > "HOLLight.hollight.int_le_def"
"int_gt_def" > "HOLLight.hollight.int_gt_def"
"int_ge_def" > "HOLLight.hollight.int_ge_def"
"int_gcd_def" > "HOLLight.hollight.int_gcd_def"
"int_eq" > "HOLLight.hollight.int.real_of_int_inject"
"int_divides_def" > "HOLLight.hollight.int_divides_def"
"int_coprime_def" > "HOLLight.hollight.int_coprime_def"
"int_congruent" > "HOLLight.hollight.int_congruent"
"int_add_th" > "HOLLight.hollight.int_add_th"
"int_add_def" > "HOLLight.hollight.int_add_def"
"int_abs_th" > "HOLLight.hollight.int_abs_th"
"int_abs_def" > "HOLLight.hollight.int_abs_def"
"hreal_of_num_def" > "HOLLight.hollight.hreal_of_num_def"
"hreal_mul_def" > "HOLLight.hollight.hreal_mul_def"
"hreal_le_def" > "HOLLight.hollight.hreal_le_def"
"hreal_inv_def" > "HOLLight.hollight.hreal_inv_def"
"hreal_add_def" > "HOLLight.hollight.hreal_add_def"
"fstcart_def" > "HOLLight.hollight.fstcart_def"
"eqeq_def" > "HOLLight.hollight.eqeq_def"
"elemma0" > "HOLLight.hollight.elemma0"
"div_def" > "HOLLight.hollight.div_def"
"dist_def" > "HOLLight.hollight.dist_def"
"dimindex_def" > "HOLLight.hollight.dimindex_def"
"dest_int_rep" > "HOLLight.hollight.dest_int_rep"
"cth" > "HOLLight.hollight.cth"
"bool_RECURSION" > "HOLLight.hollight.bool_RECURSION"
"bool_INDUCT" > "Product_Type.bool.induct"
"ax__3" > "HOL4Setup.INFINITY_AX"
"ax__2" > "Hilbert_Choice.someI"
"ax__1" > "HOL.eta_contract_eq"
"admissible_def" > "HOLLight.hollight.admissible_def"
"_UNGUARDED_PATTERN_def" > "HOLLight.hollight._UNGUARDED_PATTERN_def"
"_SEQPATTERN_def" > "HOLLight.hollight._SEQPATTERN_def"
"_MATCH_def" > "HOLLight.hollight._MATCH_def"
"_GUARDED_PATTERN_def" > "HOLLight.hollight._GUARDED_PATTERN_def"
"_FUNCTION_def" > "HOLLight.hollight._FUNCTION_def"
"_FALSITY__def" > "HOLLight.hollight._FALSITY__def"
"_11937_def" > "HOLLight.hollight._11937_def"
"ZRECSPACE_def" > "HOLLight.hollight.ZRECSPACE_def"
"ZIP" > "HOLLightList.ZIP"
"ZCONSTR_def" > "HOLLight.hollight.ZCONSTR_def"
"ZCONSTR_ZBOT" > "HOLLight.hollight.ZCONSTR_ZBOT"
"ZBOT_def" > "HOLLight.hollight.ZBOT_def"
"WLOG_LT" > "HOLLight.hollight.WLOG_LT"
"WLOG_LE" > "HOLLight.hollight.WLOG_LE"
"WF_num" > "HOLLight.hollight.WF_num"
"WF_UREC_WF" > "HOLLight.hollight.WF_UREC_WF"
"WF_UREC" > "HOLLight.hollight.WF_UREC"
"WF_SUBSET" > "HOLLight.hollight.WF_SUBSET"
"WF_REFL" > "HOLLight.hollight.WF_REFL"
"WF_REC_num" > "HOLLight.hollight.WF_REC_num"
"WF_REC_WF" > "HOLLight.hollight.WF_REC_WF"
"WF_REC_TAIL_GENERAL" > "HOLLight.hollight.WF_REC_TAIL_GENERAL"
"WF_REC_TAIL" > "HOLLight.hollight.WF_REC_TAIL"
"WF_REC_INVARIANT" > "HOLLight.hollight.WF_REC_INVARIANT"
"WF_REC" > "HOLLight.hollight.WF_REC"
"WF_POINTWISE" > "HOLLight.hollight.WF_POINTWISE"
"WF_MEASURE_GEN" > "HOLLight.hollight.WF_MEASURE_GEN"
"WF_MEASURE" > "HOLLight.hollight.WF_MEASURE"
"WF_LEX_DEPENDENT" > "HOLLight.hollight.WF_LEX_DEPENDENT"
"WF_LEX" > "HOLLight.hollight.WF_LEX"
"WF_INT_MEASURE_2" > "HOLLight.hollight.WF_INT_MEASURE_2"
"WF_INT_MEASURE" > "HOLLight.hollight.WF_INT_MEASURE"
"WF_IND" > "HOLLight.hollight.WF_IND"
"WF_FINITE" > "HOLLight.hollight.WF_FINITE"
"WF_FALSE" > "Wellfounded.wfP_empty"
"WF_EREC" > "HOLLight.hollight.WF_EREC"
"WF_EQ" > "HOLLight.hollight.WF_EQ"
"WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
"UNWIND_THM2" > "HOL.simp_thms_39"
"UNWIND_THM1" > "HOL.simp_thms_40"
"UNIV_SUBSET" > "Orderings.top_class.top_unique"
"UNIV_NOT_EMPTY" > "Set.UNIV_not_empty"
"UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
"UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
"UNION_UNIV" > "HOLLight.hollight.UNION_UNIV"
"UNION_SUBSET" > "Lattices.semilattice_sup_class.le_sup_iff"
"UNION_OVER_INTER" > "Lattices.distrib_lattice_class.distrib_3"
"UNION_IDEMPOT" > "Big_Operators.lattice_class.Sup_fin.idem"
"UNION_EMPTY" > "HOLLight.hollight.UNION_EMPTY"
"UNION_COMM" > "Lattices.lattice_class.inf_sup_aci_5"
"UNION_ASSOC" > "Lattices.lattice_class.inf_sup_aci_6"
"UNION_ACI" > "HOLLight.hollight.UNION_ACI"
"UNIONS_UNION" > "Complete_Lattices.Union_Un_distrib"
"UNIONS_SUBSET" > "HOLLight.hollight.UNIONS_SUBSET"
"UNIONS_INTERS" > "HOLLight.hollight.UNIONS_INTERS"
"UNIONS_INSERT" > "Complete_Lattices.Union_insert"
"UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
"UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
"UNIONS_2" > "Complete_Lattices.Un_eq_Union"
"UNIONS_1" > "Complete_Lattices.complete_lattice_class.Sup_singleton"
"UNIONS_0" > "Complete_Lattices.Union_empty"
"UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
"TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
"TYDEF_real" > "HOLLight.hollight.TYDEF_real"
"TYDEF_nadd" > "HOLLight.hollight.TYDEF_nadd"
"TYDEF_int" > "HOLLight.hollight.TYDEF_int"
"TYDEF_hreal" > "HOLLight.hollight.TYDEF_hreal"
"TYDEF_finite_sum" > "HOLLight.hollight.TYDEF_finite_sum"
"TYDEF_finite_image" > "HOLLight.hollight.TYDEF_finite_image"
"TYDEF_char" > "HOLLight.hollight.TYDEF_char"
"TYDEF_cart" > "HOLLight.hollight.TYDEF_cart"
"TYDEF_3" > "HOLLight.hollight.TYDEF_3"
"TYDEF_2" > "HOLLight.hollight.TYDEF_2"
"TWO" > "HOLLight.hollight.TWO"
"TRIV_OR_FORALL_THM" > "HOLLight.hollight.TRIV_OR_FORALL_THM"
"TRIV_FORALL_OR_THM" > "HOLLight.hollight.TRIV_FORALL_OR_THM"
"TRIV_FORALL_IMP_THM" > "HOLLight.hollight.TRIV_FORALL_IMP_THM"
"TRIV_EXISTS_IMP_THM" > "HOLLight.hollight.TRIV_EXISTS_IMP_THM"
"TRIV_EXISTS_AND_THM" > "HOLLight.hollight.TRIV_EXISTS_AND_THM"
"TRIV_AND_EXISTS_THM" > "HOLLight.hollight.TRIV_AND_EXISTS_THM"
"TREAL_OF_NUM_WELLDEF" > "HOLLight.hollight.TREAL_OF_NUM_WELLDEF"
"TREAL_OF_NUM_MUL" > "HOLLight.hollight.TREAL_OF_NUM_MUL"
"TREAL_OF_NUM_LE" > "HOLLight.hollight.TREAL_OF_NUM_LE"
"TREAL_OF_NUM_EQ" > "HOLLight.hollight.TREAL_OF_NUM_EQ"
"TREAL_OF_NUM_ADD" > "HOLLight.hollight.TREAL_OF_NUM_ADD"
"TREAL_NEG_WELLDEF" > "HOLLight.hollight.TREAL_NEG_WELLDEF"
"TREAL_MUL_WELLDEFR" > "HOLLight.hollight.TREAL_MUL_WELLDEFR"
"TREAL_MUL_WELLDEF" > "HOLLight.hollight.TREAL_MUL_WELLDEF"
"TREAL_MUL_SYM_EQ" > "HOLLight.hollight.TREAL_MUL_SYM_EQ"
"TREAL_MUL_SYM" > "HOLLight.hollight.TREAL_MUL_SYM"
"TREAL_MUL_LINV" > "HOLLight.hollight.TREAL_MUL_LINV"
"TREAL_MUL_LID" > "HOLLight.hollight.TREAL_MUL_LID"
"TREAL_MUL_ASSOC" > "HOLLight.hollight.TREAL_MUL_ASSOC"
"TREAL_LE_WELLDEF" > "HOLLight.hollight.TREAL_LE_WELLDEF"
"TREAL_LE_TRANS" > "HOLLight.hollight.TREAL_LE_TRANS"
"TREAL_LE_TOTAL" > "HOLLight.hollight.TREAL_LE_TOTAL"
"TREAL_LE_REFL" > "HOLLight.hollight.TREAL_LE_REFL"
"TREAL_LE_MUL" > "HOLLight.hollight.TREAL_LE_MUL"
"TREAL_LE_LADD_IMP" > "HOLLight.hollight.TREAL_LE_LADD_IMP"
"TREAL_LE_ANTISYM" > "HOLLight.hollight.TREAL_LE_ANTISYM"
"TREAL_INV_WELLDEF" > "HOLLight.hollight.TREAL_INV_WELLDEF"
"TREAL_INV_0" > "HOLLight.hollight.TREAL_INV_0"
"TREAL_EQ_TRANS" > "HOLLight.hollight.TREAL_EQ_TRANS"
"TREAL_EQ_SYM" > "HOLLight.hollight.TREAL_EQ_SYM"
"TREAL_EQ_REFL" > "HOLLight.hollight.TREAL_EQ_REFL"
"TREAL_EQ_IMP_LE" > "HOLLight.hollight.TREAL_EQ_IMP_LE"
"TREAL_EQ_AP" > "HOLLight.hollight.TREAL_EQ_AP"
"TREAL_ADD_WELLDEFR" > "HOLLight.hollight.TREAL_ADD_WELLDEFR"
"TREAL_ADD_WELLDEF" > "HOLLight.hollight.TREAL_ADD_WELLDEF"
"TREAL_ADD_SYM_EQ" > "HOLLight.hollight.TREAL_ADD_SYM_EQ"
"TREAL_ADD_SYM" > "HOLLight.hollight.TREAL_ADD_SYM"
"TREAL_ADD_LINV" > "HOLLight.hollight.TREAL_ADD_LINV"
"TREAL_ADD_LID" > "HOLLight.hollight.TREAL_ADD_LID"
"TREAL_ADD_LDISTRIB" > "HOLLight.hollight.TREAL_ADD_LDISTRIB"
"TREAL_ADD_ASSOC" > "HOLLight.hollight.TREAL_ADD_ASSOC"
"TRANSITIVE_STEPWISE_LT_EQ" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LT_EQ"
"TRANSITIVE_STEPWISE_LT" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LT"
"TRANSITIVE_STEPWISE_LE_EQ" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LE_EQ"
"TRANSITIVE_STEPWISE_LE" > "HOLLight.hollight.TRANSITIVE_STEPWISE_LE"
"TOPOLOGICAL_SORT" > "HOLLight.hollight.TOPOLOGICAL_SORT"
"SWAP_FORALL_THM" > "HOL.all_comm"
"SWAP_EXISTS_THM" > "HOL.ex_comm"
"SURJ_def" > "HOLLight.hollight.SURJ_def"
"SURJECTIVE_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_RIGHT_INVERSE"
"SURJECTIVE_ON_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_ON_RIGHT_INVERSE"
"SURJECTIVE_ON_IMAGE" > "HOLLight.hollight.SURJECTIVE_ON_IMAGE"
"SURJECTIVE_MAP" > "HOLLightList.SURJECTIVE_MAP"
"SURJECTIVE_IMAGE_THM" > "HOLLight.hollight.SURJECTIVE_IMAGE_THM"
"SURJECTIVE_IMAGE_EQ" > "HOLLight.hollight.SURJECTIVE_IMAGE_EQ"
"SURJECTIVE_IMAGE" > "HOLLight.hollight.SURJECTIVE_IMAGE"
"SURJECTIVE_IFF_INJECTIVE_GEN" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE_GEN"
"SURJECTIVE_IFF_INJECTIVE" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE"
"SURJECTIVE_FORALL_THM" > "HOLLight.hollight.SURJECTIVE_FORALL_THM"
"SURJECTIVE_EXISTS_THM" > "HOLLight.hollight.SURJECTIVE_EXISTS_THM"
"SUPPORT_SUPPORT" > "HOLLight.hollight.SUPPORT_SUPPORT"
"SUPPORT_SUBSET" > "HOLLight.hollight.SUPPORT_SUBSET"
"SUPPORT_EMPTY" > "HOLLight.hollight.SUPPORT_EMPTY"
"SUPPORT_DELTA" > "HOLLight.hollight.SUPPORT_DELTA"
"SUPPORT_CLAUSES" > "HOLLight.hollight.SUPPORT_CLAUSES"
"SUPERADMISSIBLE_TAIL" > "HOLLight.hollight.SUPERADMISSIBLE_TAIL"
"SUPERADMISSIBLE_T" > "HOLLight.hollight.SUPERADMISSIBLE_T"
"SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_UNGUARDED_PATTERN"
"SUPERADMISSIBLE_MATCH_SEQPATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_SEQPATTERN"
"SUPERADMISSIBLE_MATCH_GUARDED_PATTERN" > "HOLLight.hollight.SUPERADMISSIBLE_MATCH_GUARDED_PATTERN"
"SUPERADMISSIBLE_CONST" > "HOLLight.hollight.SUPERADMISSIBLE_CONST"
"SUPERADMISSIBLE_COND" > "HOLLight.hollight.SUPERADMISSIBLE_COND"
"SUM_ZERO_EXISTS" > "HOLLight.hollight.SUM_ZERO_EXISTS"
"SUM_UNION_RZERO" > "HOLLight.hollight.SUM_UNION_RZERO"
"SUM_UNION_NONZERO" > "HOLLight.hollight.SUM_UNION_NONZERO"
"SUM_UNION_LZERO" > "HOLLight.hollight.SUM_UNION_LZERO"
"SUM_UNION_EQ" > "HOLLight.hollight.SUM_UNION_EQ"
"SUM_UNIONS_NONZERO" > "HOLLight.hollight.SUM_UNIONS_NONZERO"
"SUM_UNION" > "HOLLight.hollight.SUM_UNION"
"SUM_TRIV_NUMSEG" > "HOLLight.hollight.SUM_TRIV_NUMSEG"
"SUM_SWAP_NUMSEG" > "HOLLight.hollight.SUM_SWAP_NUMSEG"
"SUM_SWAP" > "HOLLight.hollight.SUM_SWAP"
"SUM_SUPPORT" > "HOLLight.hollight.SUM_SUPPORT"
"SUM_SUPERSET" > "HOLLight.hollight.SUM_SUPERSET"
"SUM_SUM_RESTRICT" > "HOLLight.hollight.SUM_SUM_RESTRICT"
"SUM_SUM_PRODUCT" > "HOLLight.hollight.SUM_SUM_PRODUCT"
"SUM_SUB_NUMSEG" > "HOLLight.hollight.SUM_SUB_NUMSEG"
"SUM_SUBSET_SIMPLE" > "HOLLight.hollight.SUM_SUBSET_SIMPLE"
"SUM_SUBSET" > "HOLLight.hollight.SUM_SUBSET"
"SUM_SUB" > "HOLLight.hollight.SUM_SUB"
"SUM_SING_NUMSEG" > "HOLLight.hollight.SUM_SING_NUMSEG"
"SUM_SING" > "HOLLight.hollight.SUM_SING"
"SUM_RMUL" > "HOLLight.hollight.SUM_RMUL"
"SUM_RESTRICT_SET" > "HOLLight.hollight.SUM_RESTRICT_SET"
"SUM_RESTRICT" > "HOLLight.hollight.SUM_RESTRICT"
"SUM_POS_LE_NUMSEG" > "HOLLight.hollight.SUM_POS_LE_NUMSEG"
"SUM_POS_LE" > "HOLLight.hollight.SUM_POS_LE"
"SUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_POS_EQ_0_NUMSEG"
"SUM_POS_EQ_0" > "HOLLight.hollight.SUM_POS_EQ_0"
"SUM_POS_BOUND" > "HOLLight.hollight.SUM_POS_BOUND"
"SUM_PARTIAL_SUC" > "HOLLight.hollight.SUM_PARTIAL_SUC"
"SUM_PARTIAL_PRE" > "HOLLight.hollight.SUM_PARTIAL_PRE"
"SUM_PAIR" > "HOLLight.hollight.SUM_PAIR"
"SUM_OFFSET_0" > "HOLLight.hollight.SUM_OFFSET_0"
"SUM_OFFSET" > "HOLLight.hollight.SUM_OFFSET"
"SUM_NEG" > "HOLLight.hollight.SUM_NEG"
"SUM_MULTICOUNT_GEN" > "HOLLight.hollight.SUM_MULTICOUNT_GEN"
"SUM_MULTICOUNT" > "HOLLight.hollight.SUM_MULTICOUNT"
"SUM_LT_ALL" > "HOLLight.hollight.SUM_LT_ALL"
"SUM_LT" > "HOLLight.hollight.SUM_LT"
"SUM_LMUL" > "HOLLight.hollight.SUM_LMUL"
"SUM_LE_NUMSEG" > "HOLLight.hollight.SUM_LE_NUMSEG"
"SUM_LE_INCLUDED" > "HOLLight.hollight.SUM_LE_INCLUDED"
"SUM_LE" > "HOLLight.hollight.SUM_LE"
"SUM_INJECTION" > "HOLLight.hollight.SUM_INJECTION"
"SUM_INCL_EXCL" > "HOLLight.hollight.SUM_INCL_EXCL"
"SUM_IMAGE_NONZERO" > "HOLLight.hollight.SUM_IMAGE_NONZERO"
"SUM_IMAGE_LE" > "HOLLight.hollight.SUM_IMAGE_LE"
"SUM_IMAGE_GEN" > "HOLLight.hollight.SUM_IMAGE_GEN"
"SUM_IMAGE" > "HOLLight.hollight.SUM_IMAGE"
"SUM_GROUP" > "HOLLight.hollight.SUM_GROUP"
"SUM_EQ_SUPERSET" > "HOLLight.hollight.SUM_EQ_SUPERSET"
"SUM_EQ_NUMSEG" > "HOLLight.hollight.SUM_EQ_NUMSEG"
"SUM_EQ_GENERAL_INVERSES" > "HOLLight.hollight.SUM_EQ_GENERAL_INVERSES"
"SUM_EQ_GENERAL" > "HOLLight.hollight.SUM_EQ_GENERAL"
"SUM_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_EQ_0_NUMSEG"
"SUM_EQ_0" > "HOLLight.hollight.SUM_EQ_0"
"SUM_EQ" > "HOLLight.hollight.SUM_EQ"
"SUM_DIFFS_ALT" > "HOLLight.hollight.SUM_DIFFS_ALT"
"SUM_DIFFS" > "HOLLight.hollight.SUM_DIFFS"
"SUM_DIFF" > "HOLLight.hollight.SUM_DIFF"
"SUM_DELTA" > "HOLLight.hollight.SUM_DELTA"
"SUM_DELETE_CASES" > "HOLLight.hollight.SUM_DELETE_CASES"
"SUM_DELETE" > "HOLLight.hollight.SUM_DELETE"
"SUM_CONST_NUMSEG" > "HOLLight.hollight.SUM_CONST_NUMSEG"
"SUM_CONST" > "HOLLight.hollight.SUM_CONST"
"SUM_COMBINE_R" > "HOLLight.hollight.SUM_COMBINE_R"
"SUM_COMBINE_L" > "HOLLight.hollight.SUM_COMBINE_L"
"SUM_CLOSED" > "HOLLight.hollight.SUM_CLOSED"
"SUM_CLAUSES_RIGHT" > "HOLLight.hollight.SUM_CLAUSES_RIGHT"
"SUM_CLAUSES_NUMSEG" > "HOLLight.hollight.SUM_CLAUSES_NUMSEG"
"SUM_CLAUSES_LEFT" > "HOLLight.hollight.SUM_CLAUSES_LEFT"
"SUM_CLAUSES" > "HOLLight.hollight.SUM_CLAUSES"
"SUM_CASES_1" > "HOLLight.hollight.SUM_CASES_1"
"SUM_CASES" > "HOLLight.hollight.SUM_CASES"
"SUM_BOUND_LT_GEN" > "HOLLight.hollight.SUM_BOUND_LT_GEN"
"SUM_BOUND_LT_ALL" > "HOLLight.hollight.SUM_BOUND_LT_ALL"
"SUM_BOUND_LT" > "HOLLight.hollight.SUM_BOUND_LT"
"SUM_BOUND_GEN" > "HOLLight.hollight.SUM_BOUND_GEN"
"SUM_BOUND" > "HOLLight.hollight.SUM_BOUND"
"SUM_BIJECTION" > "HOLLight.hollight.SUM_BIJECTION"
"SUM_ADD_SPLIT" > "HOLLight.hollight.SUM_ADD_SPLIT"
"SUM_ADD_NUMSEG" > "HOLLight.hollight.SUM_ADD_NUMSEG"
"SUM_ADD_GEN" > "HOLLight.hollight.SUM_ADD_GEN"
"SUM_ADD" > "HOLLight.hollight.SUM_ADD"
"SUM_ABS_NUMSEG" > "HOLLight.hollight.SUM_ABS_NUMSEG"
"SUM_ABS_LE" > "HOLLight.hollight.SUM_ABS_LE"
"SUM_ABS_BOUND" > "HOLLight.hollight.SUM_ABS_BOUND"
"SUM_ABS" > "HOLLight.hollight.SUM_ABS"
"SUM_0" > "HOLLight.hollight.SUM_0"
"SUC_SUB1" > "Nat.diff_Suc_1"
"SUC_INJ" > "HOLLightCompat.SUC_INJ"
"SUB_SUC" > "Nat.diff_Suc_Suc"
"SUB_REFL" > "Nat.diff_self_eq_0"
"SUB_PRESUC" > "HOLLight.hollight.SUB_PRESUC"
"SUB_EQ_0" > "Nat.diff_is_0_eq"
"SUB_ELIM_THM" > "HOLLight.hollight.SUB_ELIM_THM"
"SUB_ADD_RCANCEL" > "Nat.diff_cancel2"
"SUB_ADD_LCANCEL" > "Nat.diff_cancel"
"SUB_ADD" > "Nat.le_add_diff_inverse2"
"SUB_0" > "HOLLight.hollight.SUB_0"
"SUBSET_UNIV" > "Orderings.top_class.top_greatest"
"SUBSET_UNION_ABSORPTION" > "Lattices.semilattice_sup_class.le_iff_sup"
"SUBSET_UNIONS" > "Complete_Lattices.Union_mono"
"SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
"SUBSET_TRANS" > "Orderings.order_trans_rules_23"
"SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
"SUBSET_REFL" > "Inductive.basic_monos_1"
"SUBSET_PSUBSET_TRANS" > "Orderings.order_le_less_trans"
"SUBSET_NUMSEG" > "HOLLight.hollight.SUBSET_NUMSEG"
"SUBSET_INTER_ABSORPTION" > "Lattices.semilattice_inf_class.le_iff_inf"
"SUBSET_INTER" > "Lattices.semilattice_inf_class.le_inf_iff"
"SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
"SUBSET_INSERT" > "Set.subset_insert"
"SUBSET_IMAGE" > "Set.subset_image_iff"
"SUBSET_EMPTY" > "Orderings.bot_class.bot_unique"
"SUBSET_DIFF" > "Set.Diff_subset"
"SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
"SUBSET_CARD_EQ" > "HOLLight.hollight.SUBSET_CARD_EQ"
"SUBSET_ANTISYM_EQ" > "Orderings.order_class.eq_iff"
"SUBSET_ANTISYM" > "Orderings.order_antisym"
"SND" > "Product_Type.snd_conv"
"SKOLEM_THM" > "HOLLight.hollight.SKOLEM_THM"
"SING_def" > "HOLLight.hollight.SING_def"
"SING_SUBSET" > "HOLLight.hollight.SING_SUBSET"
"SING_GSPEC" > "HOLLight.hollight.SING_GSPEC"
"SIMPLE_IMAGE_GEN" > "HOLLight.hollight.SIMPLE_IMAGE_GEN"
"SIMPLE_IMAGE" > "HOLLight.hollight.SIMPLE_IMAGE"
"SET_RECURSION_LEMMA" > "HOLLight.hollight.SET_RECURSION_LEMMA"
"SET_PROVE_CASES" > "HOLLight.hollight.SET_PROVE_CASES"
"SET_PAIR_THM" > "HOLLight.hollight.SET_PAIR_THM"
"SET_OF_LIST_MAP" > "List.set_map"
"SET_OF_LIST_EQ_EMPTY" > "List.set_empty"
"SET_OF_LIST_APPEND" > "List.set_append"
"SET_CASES" > "HOLLight.hollight.SET_CASES"
"SEMIRING_PTHS" > "HOLLight.hollight.SEMIRING_PTHS"
"SELECT_UNIQUE" > "HOLLight.hollight.SELECT_UNIQUE"
"SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
"SELECT_LEMMA" > "Hilbert_Choice.some_sym_eq_trivial"
"RIGHT_SUB_DISTRIB" > "Nat.diff_mult_distrib"
"RIGHT_OR_FORALL_THM" > "HOL.all_simps_4"
"RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
"RIGHT_OR_DISTRIB" > "Groebner_Basis.dnf_2"
"RIGHT_IMP_FORALL_THM" > "HOL.all_simps_6"
"RIGHT_IMP_EXISTS_THM" > "HOL.ex_simps_6"
"RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
"RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
"RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
"RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
"RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
"RIGHT_AND_EXISTS_THM" > "HOL.ex_simps_2"
"RIGHT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_26"
"REVERSE_REVERSE" > "List.rev_rev_ident"
"REVERSE_APPEND" > "List.rev_append"
"REST_def" > "HOLLight.hollight.REST_def"
"REFL_CLAUSE" > "Groebner_Basis.bool_simps_6"
"REAL_WLOG_LT" > "HOLLight.hollight.REAL_WLOG_LT"
"REAL_WLOG_LE" > "HOLLight.hollight.REAL_WLOG_LE"
"REAL_SUB_TRIANGLE" > "HOLLight.hollight.REAL_SUB_TRIANGLE"
"REAL_SUB_SUB2" > "HOLLight.hollight.REAL_SUB_SUB2"
"REAL_SUB_SUB" > "HOLLight.hollight.REAL_SUB_SUB"
"REAL_SUB_RZERO" > "HOLLight.hollight.REAL_SUB_RZERO"
"REAL_SUB_RNEG" > "HOLLight.hollight.REAL_SUB_RNEG"
"REAL_SUB_REFL" > "HOLLight.hollight.REAL_SUB_REFL"
"REAL_SUB_RDISTRIB" > "HOLLight.hollight.REAL_SUB_RDISTRIB"
"REAL_SUB_POW_R1" > "HOLLight.hollight.REAL_SUB_POW_R1"
"REAL_SUB_POW_L1" > "HOLLight.hollight.REAL_SUB_POW_L1"
"REAL_SUB_POW" > "HOLLight.hollight.REAL_SUB_POW"
"REAL_SUB_NEG2" > "HOLLight.hollight.REAL_SUB_NEG2"
"REAL_SUB_LZERO" > "HOLLight.hollight.REAL_SUB_LZERO"
"REAL_SUB_LT" > "HOLLight.hollight.REAL_SUB_LT"
"REAL_SUB_LNEG" > "HOLLight.hollight.REAL_SUB_LNEG"
"REAL_SUB_LE" > "HOLLight.hollight.REAL_SUB_LE"
"REAL_SUB_LDISTRIB" > "HOLLight.hollight.REAL_SUB_LDISTRIB"
"REAL_SUB_INV" > "HOLLight.hollight.REAL_SUB_INV"
"REAL_SUB_ADD2" > "HOLLight.hollight.REAL_SUB_ADD2"
"REAL_SUB_ADD" > "HOLLight.hollight.REAL_SUB_ADD"
"REAL_SUB_ABS" > "HOLLight.hollight.REAL_SUB_ABS"
"REAL_SUB_0" > "HOLLight.hollight.REAL_SUB_0"
"REAL_SOS_EQ_0" > "HOLLight.hollight.REAL_SOS_EQ_0"
"REAL_SGN_NEG" > "HOLLight.hollight.REAL_SGN_NEG"
"REAL_SGN_MUL" > "HOLLight.hollight.REAL_SGN_MUL"
"REAL_SGN_INV" > "HOLLight.hollight.REAL_SGN_INV"
"REAL_SGN_DIV" > "HOLLight.hollight.REAL_SGN_DIV"
"REAL_SGN_ABS" > "HOLLight.hollight.REAL_SGN_ABS"
"REAL_SGN_0" > "HOLLight.hollight.REAL_SGN_0"
"REAL_SGN" > "HOLLight.hollight.REAL_SGN"
"REAL_RNEG_UNIQ" > "HOLLight.hollight.REAL_RNEG_UNIQ"
"REAL_POW_ZERO" > "HOLLight.hollight.REAL_POW_ZERO"
"REAL_POW_SUB" > "HOLLight.hollight.REAL_POW_SUB"
"REAL_POW_POW" > "HOLLight.hollight.REAL_POW_POW"
"REAL_POW_ONE" > "HOLLight.hollight.REAL_POW_ONE"
"REAL_POW_NZ" > "HOLLight.hollight.REAL_POW_NZ"
"REAL_POW_NEG" > "HOLLight.hollight.REAL_POW_NEG"
"REAL_POW_MUL" > "HOLLight.hollight.REAL_POW_MUL"
"REAL_POW_MONO_LT" > "HOLLight.hollight.REAL_POW_MONO_LT"
"REAL_POW_MONO_INV" > "HOLLight.hollight.REAL_POW_MONO_INV"
"REAL_POW_MONO" > "HOLLight.hollight.REAL_POW_MONO"
"REAL_POW_LT_1" > "HOLLight.hollight.REAL_POW_LT_1"
"REAL_POW_LT2_REV" > "HOLLight.hollight.REAL_POW_LT2_REV"
"REAL_POW_LT2_ODD_EQ" > "HOLLight.hollight.REAL_POW_LT2_ODD_EQ"
"REAL_POW_LT2_ODD" > "HOLLight.hollight.REAL_POW_LT2_ODD"
"REAL_POW_LT2" > "HOLLight.hollight.REAL_POW_LT2"
"REAL_POW_LT" > "HOLLight.hollight.REAL_POW_LT"
"REAL_POW_LE_1" > "HOLLight.hollight.REAL_POW_LE_1"
"REAL_POW_LE2_REV" > "HOLLight.hollight.REAL_POW_LE2_REV"
"REAL_POW_LE2_ODD_EQ" > "HOLLight.hollight.REAL_POW_LE2_ODD_EQ"
"REAL_POW_LE2_ODD" > "HOLLight.hollight.REAL_POW_LE2_ODD"
"REAL_POW_LE2" > "HOLLight.hollight.REAL_POW_LE2"
"REAL_POW_LE" > "HOLLight.hollight.REAL_POW_LE"
"REAL_POW_INV" > "HOLLight.hollight.REAL_POW_INV"
"REAL_POW_EQ_ODD_EQ" > "HOLLight.hollight.REAL_POW_EQ_ODD_EQ"
"REAL_POW_EQ_ODD" > "HOLLight.hollight.REAL_POW_EQ_ODD"
"REAL_POW_EQ_EQ" > "HOLLight.hollight.REAL_POW_EQ_EQ"
"REAL_POW_EQ_ABS" > "HOLLight.hollight.REAL_POW_EQ_ABS"
"REAL_POW_EQ_1_IMP" > "HOLLight.hollight.REAL_POW_EQ_1_IMP"
"REAL_POW_EQ_1" > "HOLLight.hollight.REAL_POW_EQ_1"
"REAL_POW_EQ_0" > "HOLLight.hollight.REAL_POW_EQ_0"
"REAL_POW_EQ" > "HOLLight.hollight.REAL_POW_EQ"
"REAL_POW_DIV" > "HOLLight.hollight.REAL_POW_DIV"
"REAL_POW_ADD" > "HOLLight.hollight.REAL_POW_ADD"
"REAL_POW_2" > "HOLLight.hollight.REAL_POW_2"
"REAL_POW_1_LT" > "HOLLight.hollight.REAL_POW_1_LT"
"REAL_POW_1_LE" > "HOLLight.hollight.REAL_POW_1_LE"
"REAL_POW_1" > "HOLLight.hollight.REAL_POW_1"
"REAL_POW2_ABS" > "HOLLight.hollight.REAL_POW2_ABS"
"REAL_POS_NZ" > "HOLLight.hollight.REAL_POS_NZ"
"REAL_POS" > "HOLLight.hollight.REAL_POS"
"REAL_POLY_NEG_CLAUSES" > "HOLLight.hollight.REAL_POLY_NEG_CLAUSES"
"REAL_POLY_CLAUSES" > "HOLLight.hollight.REAL_POLY_CLAUSES"
"REAL_OF_NUM_SUM_NUMSEG" > "HOLLight.hollight.REAL_OF_NUM_SUM_NUMSEG"
"REAL_OF_NUM_SUM" > "HOLLight.hollight.REAL_OF_NUM_SUM"
"REAL_OF_NUM_SUC" > "HOLLight.hollight.REAL_OF_NUM_SUC"
"REAL_OF_NUM_SUB" > "HOLLight.hollight.REAL_OF_NUM_SUB"
"REAL_OF_NUM_POW" > "HOLLight.hollight.REAL_OF_NUM_POW"
"REAL_OF_NUM_MIN" > "HOLLight.hollight.REAL_OF_NUM_MIN"
"REAL_OF_NUM_MAX" > "HOLLight.hollight.REAL_OF_NUM_MAX"
"REAL_OF_NUM_LT" > "HOLLight.hollight.REAL_OF_NUM_LT"
"REAL_OF_NUM_GT" > "HOLLight.hollight.REAL_OF_NUM_GT"
"REAL_OF_NUM_GE" > "HOLLight.hollight.REAL_OF_NUM_GE"
"REAL_NOT_LT" > "HOLLight.hollight.REAL_NOT_LT"
"REAL_NOT_LE" > "HOLLight.hollight.real_lt_def"
"REAL_NOT_EQ" > "HOLLight.hollight.REAL_NOT_EQ"
"REAL_NEG_SUB" > "HOLLight.hollight.REAL_NEG_SUB"
"REAL_NEG_RMUL" > "HOLLight.hollight.REAL_NEG_RMUL"
"REAL_NEG_NEG" > "HOLLight.hollight.REAL_NEG_NEG"
"REAL_NEG_MUL2" > "HOLLight.hollight.REAL_NEG_MUL2"
"REAL_NEG_MINUS1" > "HOLLight.hollight.REAL_NEG_MINUS1"
"REAL_NEG_LT0" > "HOLLight.hollight.REAL_NEG_LT0"
"REAL_NEG_LMUL" > "HOLLight.hollight.REAL_NEG_LMUL"
"REAL_NEG_LE0" > "HOLLight.hollight.REAL_NEG_LE0"
"REAL_NEG_GT0" > "HOLLight.hollight.REAL_NEG_GT0"
"REAL_NEG_GE0" > "HOLLight.hollight.REAL_NEG_GE0"
"REAL_NEG_EQ_0" > "HOLLight.hollight.REAL_NEG_EQ_0"
"REAL_NEG_EQ" > "HOLLight.hollight.REAL_NEG_EQ"
"REAL_NEG_ADD" > "HOLLight.hollight.REAL_NEG_ADD"
"REAL_NEG_0" > "HOLLight.hollight.REAL_NEG_0"
"REAL_NEGNEG" > "HOLLight.hollight.REAL_NEGNEG"
"REAL_MUL_RZERO" > "HOLLight.hollight.REAL_MUL_RZERO"
"REAL_MUL_RNEG" > "HOLLight.hollight.REAL_MUL_RNEG"
"REAL_MUL_RINV_UNIQ" > "HOLLight.hollight.REAL_MUL_RINV_UNIQ"
"REAL_MUL_RINV" > "HOLLight.hollight.REAL_MUL_RINV"
"REAL_MUL_RID" > "HOLLight.hollight.REAL_MUL_RID"
"REAL_MUL_POS_LT" > "HOLLight.hollight.REAL_MUL_POS_LT"
"REAL_MUL_POS_LE" > "HOLLight.hollight.REAL_MUL_POS_LE"
"REAL_MUL_LZERO" > "HOLLight.hollight.REAL_MUL_LZERO"
"REAL_MUL_LNEG" > "HOLLight.hollight.REAL_MUL_LNEG"
"REAL_MUL_LINV_UNIQ" > "HOLLight.hollight.REAL_MUL_LINV_UNIQ"
"REAL_MUL_AC" > "HOLLight.hollight.REAL_MUL_AC"
"REAL_MUL_2" > "HOLLight.hollight.REAL_MUL_2"
"REAL_MIN_SYM" > "HOLLight.hollight.REAL_MIN_SYM"
"REAL_MIN_MIN" > "HOLLight.hollight.REAL_MIN_MIN"
"REAL_MIN_MAX" > "HOLLight.hollight.REAL_MIN_MAX"
"REAL_MIN_LT" > "HOLLight.hollight.REAL_MIN_LT"
"REAL_MIN_LE" > "HOLLight.hollight.REAL_MIN_LE"
"REAL_MIN_ASSOC" > "HOLLight.hollight.REAL_MIN_ASSOC"
"REAL_MIN_ACI" > "HOLLight.hollight.REAL_MIN_ACI"
"REAL_MAX_SYM" > "HOLLight.hollight.REAL_MAX_SYM"
"REAL_MAX_MIN" > "HOLLight.hollight.REAL_MAX_MIN"
"REAL_MAX_MAX" > "HOLLight.hollight.REAL_MAX_MAX"
"REAL_MAX_LT" > "HOLLight.hollight.REAL_MAX_LT"
"REAL_MAX_LE" > "HOLLight.hollight.REAL_MAX_LE"
"REAL_MAX_ASSOC" > "HOLLight.hollight.REAL_MAX_ASSOC"
"REAL_MAX_ACI" > "HOLLight.hollight.REAL_MAX_ACI"
"REAL_LT_TRANS" > "HOLLight.hollight.REAL_LT_TRANS"
"REAL_LT_TOTAL" > "HOLLight.hollight.REAL_LT_TOTAL"
"REAL_LT_SUB_RADD" > "HOLLight.hollight.REAL_LT_SUB_RADD"
"REAL_LT_SUB_LADD" > "HOLLight.hollight.REAL_LT_SUB_LADD"
"REAL_LT_SQUARE_ABS" > "HOLLight.hollight.REAL_LT_SQUARE_ABS"
"REAL_LT_SQUARE" > "HOLLight.hollight.REAL_LT_SQUARE"
"REAL_LT_RNEG" > "HOLLight.hollight.REAL_LT_RNEG"
"REAL_LT_RMUL_EQ" > "HOLLight.hollight.REAL_LT_RMUL_EQ"
"REAL_LT_RMUL" > "HOLLight.hollight.REAL_LT_RMUL"
"REAL_LT_RINV" > "HOLLight.hollight.REAL_LT_RINV"
"REAL_LT_REFL" > "HOLLight.hollight.REAL_LT_REFL"
"REAL_LT_RDIV_EQ" > "HOLLight.hollight.REAL_LT_RDIV_EQ"
"REAL_LT_RCANCEL_IMP" > "HOLLight.hollight.REAL_LT_RCANCEL_IMP"
"REAL_LT_RADD" > "HOLLight.hollight.REAL_LT_RADD"
"REAL_LT_POW2" > "HOLLight.hollight.REAL_LT_POW2"
"REAL_LT_NEGTOTAL" > "HOLLight.hollight.REAL_LT_NEGTOTAL"
"REAL_LT_NEG2" > "HOLLight.hollight.REAL_LT_NEG2"
"REAL_LT_NEG" > "HOLLight.hollight.REAL_LT_NEG"
"REAL_LT_MUL_EQ" > "HOLLight.hollight.REAL_LT_MUL_EQ"
"REAL_LT_MUL2" > "HOLLight.hollight.REAL_LT_MUL2"
"REAL_LT_MUL" > "HOLLight.hollight.REAL_LT_MUL"
"REAL_LT_MIN" > "HOLLight.hollight.REAL_LT_MIN"
"REAL_LT_MAX" > "HOLLight.hollight.REAL_LT_MAX"
"REAL_LT_LNEG" > "HOLLight.hollight.REAL_LT_LNEG"
"REAL_LT_LMUL_EQ" > "HOLLight.hollight.REAL_LT_LMUL_EQ"
"REAL_LT_LMUL" > "HOLLight.hollight.REAL_LT_LMUL"
"REAL_LT_LINV" > "HOLLight.hollight.REAL_LT_LINV"
"REAL_LT_LE" > "HOLLight.hollight.REAL_LT_LE"
"REAL_LT_LDIV_EQ" > "HOLLight.hollight.REAL_LT_LDIV_EQ"
"REAL_LT_LCANCEL_IMP" > "HOLLight.hollight.REAL_LT_LCANCEL_IMP"
"REAL_LT_LADD_IMP" > "HOLLight.hollight.REAL_LT_LADD_IMP"
"REAL_LT_LADD" > "HOLLight.hollight.REAL_LT_LADD"
"REAL_LT_INV_EQ" > "HOLLight.hollight.REAL_LT_INV_EQ"
"REAL_LT_INV2" > "HOLLight.hollight.REAL_LT_INV2"
"REAL_LT_INV" > "HOLLight.hollight.REAL_LT_INV"
"REAL_LT_IMP_NZ" > "HOLLight.hollight.REAL_LT_IMP_NZ"
"REAL_LT_IMP_NE" > "HOLLight.hollight.REAL_LT_IMP_NE"
"REAL_LT_IMP_LE" > "HOLLight.hollight.REAL_LT_IMP_LE"
"REAL_LT_GT" > "HOLLight.hollight.REAL_LT_GT"
"REAL_LT_DIV2_EQ" > "HOLLight.hollight.REAL_LT_DIV2_EQ"
"REAL_LT_DIV" > "HOLLight.hollight.REAL_LT_DIV"
"REAL_LT_ANTISYM" > "HOLLight.hollight.REAL_LT_ANTISYM"
"REAL_LT_ADD_SUB" > "HOLLight.hollight.REAL_LT_ADD_SUB"
"REAL_LT_ADDR" > "HOLLight.hollight.REAL_LT_ADDR"
"REAL_LT_ADDNEG2" > "HOLLight.hollight.REAL_LT_ADDNEG2"
"REAL_LT_ADDNEG" > "HOLLight.hollight.REAL_LT_ADDNEG"
"REAL_LT_ADDL" > "HOLLight.hollight.REAL_LT_ADDL"
"REAL_LT_ADD2" > "HOLLight.hollight.REAL_LT_ADD2"
"REAL_LT_ADD1" > "HOLLight.hollight.REAL_LT_ADD1"
"REAL_LT_ADD" > "HOLLight.hollight.REAL_LT_ADD"
"REAL_LT_01" > "HOLLight.hollight.REAL_LT_01"
"REAL_LTE_TRANS" > "HOLLight.hollight.REAL_LTE_TRANS"
"REAL_LTE_TOTAL" > "HOLLight.hollight.REAL_LTE_TOTAL"
"REAL_LTE_ANTISYM" > "HOLLight.hollight.REAL_LTE_ANTISYM"
"REAL_LTE_ADD2" > "HOLLight.hollight.REAL_LTE_ADD2"
"REAL_LTE_ADD" > "HOLLight.hollight.REAL_LTE_ADD"
"REAL_LNEG_UNIQ" > "HOLLight.hollight.REAL_LNEG_UNIQ"
"REAL_LE_SUB_RADD" > "HOLLight.hollight.REAL_LE_SUB_RADD"
"REAL_LE_SUB_LADD" > "HOLLight.hollight.REAL_LE_SUB_LADD"
"REAL_LE_SQUARE_ABS" > "HOLLight.hollight.REAL_LE_SQUARE_ABS"
"REAL_LE_SQUARE" > "HOLLight.hollight.REAL_LE_SQUARE"
"REAL_LE_RNEG" > "HOLLight.hollight.REAL_LE_RNEG"
"REAL_LE_RMUL_EQ" > "HOLLight.hollight.REAL_LE_RMUL_EQ"
"REAL_LE_RMUL" > "HOLLight.hollight.REAL_LE_RMUL"
"REAL_LE_RINV" > "HOLLight.hollight.REAL_LE_RINV"
"REAL_LE_RDIV_EQ" > "HOLLight.hollight.REAL_LE_RDIV_EQ"
"REAL_LE_RCANCEL_IMP" > "HOLLight.hollight.REAL_LE_RCANCEL_IMP"
"REAL_LE_RADD" > "HOLLight.hollight.REAL_LE_RADD"
"REAL_LE_POW_2" > "HOLLight.hollight.REAL_LE_POW_2"
"REAL_LE_POW2" > "HOLLight.hollight.REAL_LE_POW2"
"REAL_LE_NEGTOTAL" > "HOLLight.hollight.REAL_LE_NEGTOTAL"
"REAL_LE_NEGR" > "HOLLight.hollight.REAL_LE_NEGR"
"REAL_LE_NEGL" > "HOLLight.hollight.REAL_LE_NEGL"
"REAL_LE_NEG2" > "HOLLight.hollight.REAL_LE_NEG2"
"REAL_LE_NEG" > "HOLLight.hollight.REAL_LE_NEG"
"REAL_LE_MUL_EQ" > "HOLLight.hollight.REAL_LE_MUL_EQ"
"REAL_LE_MUL2" > "HOLLight.hollight.REAL_LE_MUL2"
"REAL_LE_MIN" > "HOLLight.hollight.REAL_LE_MIN"
"REAL_LE_MAX" > "HOLLight.hollight.REAL_LE_MAX"
"REAL_LE_LT" > "HOLLight.hollight.REAL_LE_LT"
"REAL_LE_LNEG" > "HOLLight.hollight.REAL_LE_LNEG"
"REAL_LE_LMUL_EQ" > "HOLLight.hollight.REAL_LE_LMUL_EQ"
"REAL_LE_LMUL" > "HOLLight.hollight.REAL_LE_LMUL"
"REAL_LE_LINV" > "HOLLight.hollight.REAL_LE_LINV"
"REAL_LE_LDIV_EQ" > "HOLLight.hollight.REAL_LE_LDIV_EQ"
"REAL_LE_LCANCEL_IMP" > "HOLLight.hollight.REAL_LE_LCANCEL_IMP"
"REAL_LE_LADD" > "HOLLight.hollight.REAL_LE_LADD"
"REAL_LE_INV_EQ" > "HOLLight.hollight.REAL_LE_INV_EQ"
"REAL_LE_INV2" > "HOLLight.hollight.REAL_LE_INV2"
"REAL_LE_INV" > "HOLLight.hollight.REAL_LE_INV"
"REAL_LE_DOUBLE" > "HOLLight.hollight.REAL_LE_DOUBLE"
"REAL_LE_DIV2_EQ" > "HOLLight.hollight.REAL_LE_DIV2_EQ"
"REAL_LE_DIV" > "HOLLight.hollight.REAL_LE_DIV"
"REAL_LE_ADDR" > "HOLLight.hollight.REAL_LE_ADDR"
"REAL_LE_ADDL" > "HOLLight.hollight.REAL_LE_ADDL"
"REAL_LE_ADD2" > "HOLLight.hollight.REAL_LE_ADD2"
"REAL_LE_ADD" > "HOLLight.hollight.REAL_LE_ADD"
"REAL_LE_01" > "HOLLight.hollight.REAL_LE_01"
"REAL_LET_TRANS" > "HOLLight.hollight.REAL_LET_TRANS"
"REAL_LET_TOTAL" > "HOLLight.hollight.REAL_LET_TOTAL"
"REAL_LET_ANTISYM" > "HOLLight.hollight.REAL_LET_ANTISYM"
"REAL_LET_ADD2" > "HOLLight.hollight.REAL_LET_ADD2"
"REAL_LET_ADD" > "HOLLight.hollight.REAL_LET_ADD"
"REAL_INV_POW" > "HOLLight.hollight.REAL_INV_POW"
"REAL_INV_NEG" > "HOLLight.hollight.REAL_INV_NEG"
"REAL_INV_MUL" > "HOLLight.hollight.REAL_INV_MUL"
"REAL_INV_LT_1" > "HOLLight.hollight.REAL_INV_LT_1"
"REAL_INV_LE_1" > "HOLLight.hollight.REAL_INV_LE_1"
"REAL_INV_INV" > "HOLLight.hollight.REAL_INV_INV"
"REAL_INV_EQ_1" > "HOLLight.hollight.REAL_INV_EQ_1"
"REAL_INV_EQ_0" > "HOLLight.hollight.REAL_INV_EQ_0"
"REAL_INV_DIV" > "HOLLight.hollight.REAL_INV_DIV"
"REAL_INV_1_LT" > "HOLLight.hollight.REAL_INV_1_LT"
"REAL_INV_1_LE" > "HOLLight.hollight.REAL_INV_1_LE"
"REAL_INV_1" > "HOLLight.hollight.REAL_INV_1"
"REAL_INTEGRAL" > "HOLLight.hollight.REAL_INTEGRAL"
"REAL_HREAL_LEMMA2" > "HOLLight.hollight.REAL_HREAL_LEMMA2"
"REAL_HREAL_LEMMA1" > "HOLLight.hollight.REAL_HREAL_LEMMA1"
"REAL_EQ_SUB_RADD" > "HOLLight.hollight.REAL_EQ_SUB_RADD"
"REAL_EQ_SUB_LADD" > "HOLLight.hollight.REAL_EQ_SUB_LADD"
"REAL_EQ_SQUARE_ABS" > "HOLLight.hollight.REAL_EQ_SQUARE_ABS"
"REAL_EQ_RDIV_EQ" > "HOLLight.hollight.REAL_EQ_RDIV_EQ"
"REAL_EQ_RCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_RCANCEL_IMP"
"REAL_EQ_NEG2" > "HOLLight.hollight.REAL_EQ_NEG2"
"REAL_EQ_MUL_RCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_RCANCEL"
"REAL_EQ_MUL_LCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_LCANCEL"
"REAL_EQ_LDIV_EQ" > "HOLLight.hollight.REAL_EQ_LDIV_EQ"
"REAL_EQ_LCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_LCANCEL_IMP"
"REAL_EQ_INV2" > "HOLLight.hollight.REAL_EQ_INV2"
"REAL_EQ_IMP_LE" > "HOLLight.hollight.REAL_EQ_IMP_LE"
"REAL_EQ_ADD_RCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL_0"
"REAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL"
"REAL_EQ_ADD_LCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL_0"
"REAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL"
"REAL_ENTIRE" > "HOLLight.hollight.REAL_ENTIRE"
"REAL_DOWN2" > "HOLLight.hollight.REAL_DOWN2"
"REAL_DOWN" > "HOLLight.hollight.REAL_DOWN"
"REAL_DIV_RMUL" > "HOLLight.hollight.REAL_DIV_RMUL"
"REAL_DIV_REFL" > "HOLLight.hollight.REAL_DIV_REFL"
"REAL_DIV_POW2_ALT" > "HOLLight.hollight.REAL_DIV_POW2_ALT"
"REAL_DIV_POW2" > "HOLLight.hollight.REAL_DIV_POW2"
"REAL_DIV_LMUL" > "HOLLight.hollight.REAL_DIV_LMUL"
"REAL_DIV_1" > "HOLLight.hollight.REAL_DIV_1"
"REAL_DIFFSQ" > "HOLLight.hollight.REAL_DIFFSQ"
"REAL_COMPLETE_SOMEPOS" > "HOLLight.hollight.REAL_COMPLETE_SOMEPOS"
"REAL_COMPLETE" > "HOLLight.hollight.REAL_COMPLETE"
"REAL_BOUNDS_LT" > "HOLLight.hollight.REAL_BOUNDS_LT"
"REAL_BOUNDS_LE" > "HOLLight.hollight.REAL_BOUNDS_LE"
"REAL_ADD_SUB2" > "HOLLight.hollight.REAL_ADD_SUB2"
"REAL_ADD_SUB" > "HOLLight.hollight.REAL_ADD_SUB"
"REAL_ADD_RINV" > "HOLLight.hollight.REAL_ADD_RINV"
"REAL_ADD_RID" > "HOLLight.hollight.REAL_ADD_RID"
"REAL_ADD_RDISTRIB" > "HOLLight.hollight.REAL_ADD_RDISTRIB"
"REAL_ADD_AC" > "HOLLight.hollight.REAL_ADD_AC"
"REAL_ADD2_SUB2" > "HOLLight.hollight.REAL_ADD2_SUB2"
"REAL_ABS_ZERO" > "HOLLight.hollight.REAL_ABS_ZERO"
"REAL_ABS_TRIANGLE_LT" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LT"
"REAL_ABS_TRIANGLE_LE" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LE"
"REAL_ABS_TRIANGLE" > "HOLLight.hollight.REAL_ABS_TRIANGLE"
"REAL_ABS_SUB_ABS" > "HOLLight.hollight.REAL_ABS_SUB_ABS"
"REAL_ABS_SUB" > "HOLLight.hollight.REAL_ABS_SUB"
"REAL_ABS_STILLNZ" > "HOLLight.hollight.REAL_ABS_STILLNZ"
"REAL_ABS_SIGN2" > "HOLLight.hollight.REAL_ABS_SIGN2"
"REAL_ABS_SIGN" > "HOLLight.hollight.REAL_ABS_SIGN"
"REAL_ABS_SGN" > "HOLLight.hollight.REAL_ABS_SGN"
"REAL_ABS_REFL" > "HOLLight.hollight.REAL_ABS_REFL"
"REAL_ABS_POW" > "HOLLight.hollight.REAL_ABS_POW"
"REAL_ABS_POS" > "HOLLight.hollight.REAL_ABS_POS"
"REAL_ABS_NZ" > "HOLLight.hollight.REAL_ABS_NZ"
"REAL_ABS_NUM" > "HOLLight.hollight.REAL_ABS_NUM"
"REAL_ABS_NEG" > "HOLLight.hollight.REAL_ABS_NEG"
"REAL_ABS_MUL" > "HOLLight.hollight.REAL_ABS_MUL"
"REAL_ABS_LE" > "HOLLight.hollight.REAL_ABS_LE"
"REAL_ABS_INV" > "HOLLight.hollight.REAL_ABS_INV"
"REAL_ABS_DIV" > "HOLLight.hollight.REAL_ABS_DIV"
"REAL_ABS_CIRCLE" > "HOLLight.hollight.REAL_ABS_CIRCLE"
"REAL_ABS_CASES" > "HOLLight.hollight.REAL_ABS_CASES"
"REAL_ABS_BOUNDS" > "HOLLight.hollight.REAL_ABS_BOUNDS"
"REAL_ABS_BOUND" > "HOLLight.hollight.REAL_ABS_BOUND"
"REAL_ABS_BETWEEN2" > "HOLLight.hollight.REAL_ABS_BETWEEN2"
"REAL_ABS_BETWEEN1" > "HOLLight.hollight.REAL_ABS_BETWEEN1"
"REAL_ABS_BETWEEN" > "HOLLight.hollight.REAL_ABS_BETWEEN"
"REAL_ABS_ABS" > "HOLLight.hollight.REAL_ABS_ABS"
"REAL_ABS_1" > "HOLLight.hollight.REAL_ABS_1"
"REAL_ABS_0" > "HOLLight.hollight.REAL_ABS_0"
"RAT_LEMMA5" > "HOLLight.hollight.RAT_LEMMA5"
"RAT_LEMMA4" > "HOLLight.hollight.RAT_LEMMA4"
"RAT_LEMMA3" > "HOLLight.hollight.RAT_LEMMA3"
"RAT_LEMMA2" > "HOLLight.hollight.RAT_LEMMA2"
"RAT_LEMMA1" > "HOLLight.hollight.RAT_LEMMA1"
"PSUBSET_UNIV" > "HOLLight.hollight.PSUBSET_UNIV"
"PSUBSET_TRANS" > "Orderings.order_less_trans"
"PSUBSET_SUBSET_TRANS" > "Orderings.order_less_le_trans"
"PSUBSET_MEMBER" > "HOLLight.hollight.PSUBSET_MEMBER"
"PSUBSET_IRREFL" > "Orderings.order_less_irrefl"
"PSUBSET_INSERT_SUBSET" > "HOLLight.hollight.PSUBSET_INSERT_SUBSET"
"PSUBSET_ALT" > "HOLLight.hollight.PSUBSET_ALT"
"PRE_ELIM_THM" > "HOLLight.hollight.PRE_ELIM_THM"
"POWERSET_CLAUSES" > "HOLLight.hollight.POWERSET_CLAUSES"
"PASSOC_def" > "HOLLight.hollight.PASSOC_def"
"PAIR_SURJECTIVE" > "Product_Type.prod.nchotomy"
"PAIR_EXISTS_THM" > "HOLLight.hollight.PAIR_EXISTS_THM"
"PAIR_EQ" > "Product_Type.Pair_eq"
"PAIRWISE_def" > "HOLLight.hollight.PAIRWISE_def"
"PAIRWISE_SING" > "HOLLight.hollight.PAIRWISE_SING"
"PAIRWISE_MONO" > "HOLLight.hollight.PAIRWISE_MONO"
"PAIRWISE_EMPTY" > "HOLLight.hollight.PAIRWISE_EMPTY"
"PAIR" > "HOLLightCompat.PAIR"
"OR_EXISTS_THM" > "HOL.ex_disj_distrib"
"OR_CLAUSES" > "HOLLight.hollight.OR_CLAUSES"
"ONE" > "Nat.One_nat_def"
"ODD_SUB" > "HOLLight.hollight.ODD_SUB"
"ODD_MULT" > "HOLLight.hollight.ODD_MULT"
"ODD_MOD" > "HOLLight.hollight.ODD_MOD"
"ODD_EXP" > "HOLLight.hollight.ODD_EXP"
"ODD_EXISTS" > "Parity.odd_Suc_mult_two_ex"
"ODD_DOUBLE" > "HOLLight.hollight.ODD_DOUBLE"
"ODD_ADD" > "Parity.odd_add"
"NUM_REP_def" > "HOLLight.hollight.NUM_REP_def"
"NUM_OF_INT_OF_NUM" > "HOLLight.hollight.NUM_OF_INT_OF_NUM"
"NUM_OF_INT" > "HOLLight.hollight.NUM_OF_INT"
"NUM_INTEGRAL_LEMMA" > "HOLLight.hollight.NUM_INTEGRAL_LEMMA"
"NUM_INTEGRAL" > "HOLLight.hollight.NUM_INTEGRAL"
"NUM_GCD" > "HOLLight.hollight.NUM_GCD"
"NUMSUM_def" > "HOLLight.hollight.NUMSUM_def"
"NUMSUM_INJ" > "HOLLight.hollight.NUMSUM_INJ"
"NUMSND_def" > "HOLLight.hollight.NUMSND_def"
"NUMSEG_SING" > "SetInterval.order_class.atLeastAtMost_singleton"
"NUMSEG_RREC" > "HOLLight.hollight.NUMSEG_RREC"
"NUMSEG_REC" > "SetInterval.atLeastAtMostSuc_conv"
"NUMSEG_OFFSET_IMAGE" > "SetInterval.image_add_atLeastAtMost"
"NUMSEG_LT" > "HOLLight.hollight.NUMSEG_LT"
"NUMSEG_LREC" > "HOLLight.hollight.NUMSEG_LREC"
"NUMSEG_LE" > "HOLLight.hollight.NUMSEG_LE"
"NUMSEG_EMPTY" > "HOLLight.hollight.NUMSEG_EMPTY"
"NUMSEG_COMBINE_R" > "HOLLight.hollight.NUMSEG_COMBINE_R"
"NUMSEG_COMBINE_L" > "HOLLight.hollight.NUMSEG_COMBINE_L"
"NUMSEG_CLAUSES" > "HOLLight.hollight.NUMSEG_CLAUSES"
"NUMSEG_ADD_SPLIT" > "HOLLight.hollight.NUMSEG_ADD_SPLIT"
"NUMRIGHT_def" > "HOLLight.hollight.NUMRIGHT_def"
"NUMPAIR_def" > "HOLLight.hollight.NUMPAIR_def"
"NUMPAIR_INJ_LEMMA" > "HOLLight.hollight.NUMPAIR_INJ_LEMMA"
"NUMPAIR_INJ" > "HOLLight.hollight.NUMPAIR_INJ"
"NUMLEFT_def" > "HOLLight.hollight.NUMLEFT_def"
"NUMFST_def" > "HOLLight.hollight.NUMFST_def"
"NSUM_UNION_RZERO" > "HOLLight.hollight.NSUM_UNION_RZERO"
"NSUM_UNION_NONZERO" > "HOLLight.hollight.NSUM_UNION_NONZERO"
"NSUM_UNION_LZERO" > "HOLLight.hollight.NSUM_UNION_LZERO"
"NSUM_UNION_EQ" > "HOLLight.hollight.NSUM_UNION_EQ"
"NSUM_UNIONS_NONZERO" > "HOLLight.hollight.NSUM_UNIONS_NONZERO"
"NSUM_UNION" > "HOLLight.hollight.NSUM_UNION"
"NSUM_TRIV_NUMSEG" > "HOLLight.hollight.NSUM_TRIV_NUMSEG"
"NSUM_SWAP_NUMSEG" > "HOLLight.hollight.NSUM_SWAP_NUMSEG"
"NSUM_SWAP" > "HOLLight.hollight.NSUM_SWAP"
"NSUM_SUPPORT" > "HOLLight.hollight.NSUM_SUPPORT"
"NSUM_SUPERSET" > "HOLLight.hollight.NSUM_SUPERSET"
"NSUM_SUBSET_SIMPLE" > "HOLLight.hollight.NSUM_SUBSET_SIMPLE"
"NSUM_SUBSET" > "HOLLight.hollight.NSUM_SUBSET"
"NSUM_SING_NUMSEG" > "HOLLight.hollight.NSUM_SING_NUMSEG"
"NSUM_SING" > "HOLLight.hollight.NSUM_SING"
"NSUM_RMUL" > "HOLLight.hollight.NSUM_RMUL"
"NSUM_RESTRICT_SET" > "HOLLight.hollight.NSUM_RESTRICT_SET"
"NSUM_RESTRICT" > "HOLLight.hollight.NSUM_RESTRICT"
"NSUM_POS_BOUND" > "HOLLight.hollight.NSUM_POS_BOUND"
"NSUM_PAIR" > "HOLLight.hollight.NSUM_PAIR"
"NSUM_OFFSET_0" > "HOLLight.hollight.NSUM_OFFSET_0"
"NSUM_OFFSET" > "HOLLight.hollight.NSUM_OFFSET"
"NSUM_NSUM_RESTRICT" > "HOLLight.hollight.NSUM_NSUM_RESTRICT"
"NSUM_NSUM_PRODUCT" > "HOLLight.hollight.NSUM_NSUM_PRODUCT"
"NSUM_MULTICOUNT_GEN" > "HOLLight.hollight.NSUM_MULTICOUNT_GEN"
"NSUM_MULTICOUNT" > "HOLLight.hollight.NSUM_MULTICOUNT"
"NSUM_LT_ALL" > "HOLLight.hollight.NSUM_LT_ALL"
"NSUM_LT" > "HOLLight.hollight.NSUM_LT"
"NSUM_LMUL" > "HOLLight.hollight.NSUM_LMUL"
"NSUM_LE_NUMSEG" > "HOLLight.hollight.NSUM_LE_NUMSEG"
"NSUM_LE" > "HOLLight.hollight.NSUM_LE"
"NSUM_INJECTION" > "HOLLight.hollight.NSUM_INJECTION"
"NSUM_INCL_EXCL" > "HOLLight.hollight.NSUM_INCL_EXCL"
"NSUM_IMAGE_NONZERO" > "HOLLight.hollight.NSUM_IMAGE_NONZERO"
"NSUM_IMAGE_GEN" > "HOLLight.hollight.NSUM_IMAGE_GEN"
"NSUM_IMAGE" > "HOLLight.hollight.NSUM_IMAGE"
"NSUM_GROUP" > "HOLLight.hollight.NSUM_GROUP"
"NSUM_EQ_SUPERSET" > "HOLLight.hollight.NSUM_EQ_SUPERSET"
"NSUM_EQ_NUMSEG" > "HOLLight.hollight.NSUM_EQ_NUMSEG"
"NSUM_EQ_GENERAL_INVERSES" > "HOLLight.hollight.NSUM_EQ_GENERAL_INVERSES"
"NSUM_EQ_GENERAL" > "HOLLight.hollight.NSUM_EQ_GENERAL"
"NSUM_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_NUMSEG"
"NSUM_EQ_0_IFF_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_IFF_NUMSEG"
"NSUM_EQ_0_IFF" > "HOLLight.hollight.NSUM_EQ_0_IFF"
"NSUM_EQ_0" > "HOLLight.hollight.NSUM_EQ_0"
"NSUM_EQ" > "HOLLight.hollight.NSUM_EQ"
"NSUM_DIFF" > "HOLLight.hollight.NSUM_DIFF"
"NSUM_DELTA" > "HOLLight.hollight.NSUM_DELTA"
"NSUM_DELETE" > "HOLLight.hollight.NSUM_DELETE"
"NSUM_CONST_NUMSEG" > "HOLLight.hollight.NSUM_CONST_NUMSEG"
"NSUM_CONST" > "HOLLight.hollight.NSUM_CONST"
"NSUM_CLOSED" > "HOLLight.hollight.NSUM_CLOSED"
"NSUM_CLAUSES_RIGHT" > "HOLLight.hollight.NSUM_CLAUSES_RIGHT"
"NSUM_CLAUSES_NUMSEG" > "HOLLight.hollight.NSUM_CLAUSES_NUMSEG"
"NSUM_CLAUSES_LEFT" > "HOLLight.hollight.NSUM_CLAUSES_LEFT"
"NSUM_CLAUSES" > "HOLLight.hollight.NSUM_CLAUSES"
"NSUM_CASES" > "HOLLight.hollight.NSUM_CASES"
"NSUM_BOUND_LT_GEN" > "HOLLight.hollight.NSUM_BOUND_LT_GEN"
"NSUM_BOUND_LT_ALL" > "HOLLight.hollight.NSUM_BOUND_LT_ALL"
"NSUM_BOUND_LT" > "HOLLight.hollight.NSUM_BOUND_LT"
"NSUM_BOUND_GEN" > "HOLLight.hollight.NSUM_BOUND_GEN"
"NSUM_BOUND" > "HOLLight.hollight.NSUM_BOUND"
"NSUM_BIJECTION" > "HOLLight.hollight.NSUM_BIJECTION"
"NSUM_ADD_SPLIT" > "HOLLight.hollight.NSUM_ADD_SPLIT"
"NSUM_ADD_NUMSEG" > "HOLLight.hollight.NSUM_ADD_NUMSEG"
"NSUM_ADD_GEN" > "HOLLight.hollight.NSUM_ADD_GEN"
"NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
"NSUM_0" > "HOLLight.hollight.NSUM_0"
"NOT_UNIV_PSUBSET" > "Orderings.top_class.not_top_less"
"NOT_SUC" > "Nat.Suc_not_Zero"
"NOT_PSUBSET_EMPTY" > "Orderings.bot_class.not_less_bot"
"NOT_ODD" > "HOLLight.hollight.NOT_ODD"
"NOT_LT" > "Orderings.linorder_class.not_less"
"NOT_LE" > "Orderings.linorder_class.not_le"
"NOT_IN_EMPTY" > "HOLLight.hollight.NOT_IN_EMPTY"
"NOT_INSERT_EMPTY" > "Set.insert_not_empty"
"NOT_FORALL_THM" > "HOL.not_all"
"NOT_EXISTS_THM" > "HOL.not_ex"
"NOT_EX" > "HOLLightList.NOT_EX"
"NOT_EVEN" > "HOLLight.hollight.NOT_EVEN"
"NOT_EQUAL_SETS" > "HOLLight.hollight.NOT_EQUAL_SETS"
"NOT_EMPTY_INSERT" > "Set.empty_not_insert"
"NOT_CONS_NIL" > "List.list.distinct_2"
"NOT_CLAUSES_WEAK" > "HOLLight.hollight.NOT_CLAUSES_WEAK"
"NOT_ALL" > "HOLLightList.NOT_ALL"
"NEUTRAL_REAL_MUL" > "HOLLight.hollight.NEUTRAL_REAL_MUL"
"NEUTRAL_REAL_ADD" > "HOLLight.hollight.NEUTRAL_REAL_ADD"
"NEUTRAL_MUL" > "HOLLight.hollight.NEUTRAL_MUL"
"NEUTRAL_ADD" > "HOLLight.hollight.NEUTRAL_ADD"
"NADD_UBOUND" > "HOLLight.hollight.NADD_UBOUND"
"NADD_SUC" > "HOLLight.hollight.NADD_SUC"
"NADD_RDISTRIB" > "HOLLight.hollight.NADD_RDISTRIB"
"NADD_OF_NUM_WELLDEF" > "HOLLight.hollight.NADD_OF_NUM_WELLDEF"
"NADD_OF_NUM_MUL" > "HOLLight.hollight.NADD_OF_NUM_MUL"
"NADD_OF_NUM_LE" > "HOLLight.hollight.NADD_OF_NUM_LE"
"NADD_OF_NUM_EQ" > "HOLLight.hollight.NADD_OF_NUM_EQ"
"NADD_OF_NUM_ADD" > "HOLLight.hollight.NADD_OF_NUM_ADD"
"NADD_OF_NUM" > "HOLLight.hollight.NADD_OF_NUM"
"NADD_NONZERO" > "HOLLight.hollight.NADD_NONZERO"
"NADD_MUL_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_MUL_WELLDEF_LEMMA"
"NADD_MUL_WELLDEF" > "HOLLight.hollight.NADD_MUL_WELLDEF"
"NADD_MUL_SYM" > "HOLLight.hollight.NADD_MUL_SYM"
"NADD_MUL_LINV_LEMMA8" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA8"
"NADD_MUL_LINV_LEMMA7a" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7a"
"NADD_MUL_LINV_LEMMA7" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7"
"NADD_MUL_LINV_LEMMA6" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA6"
"NADD_MUL_LINV_LEMMA5" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA5"
"NADD_MUL_LINV_LEMMA4" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA4"
"NADD_MUL_LINV_LEMMA3" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA3"
"NADD_MUL_LINV_LEMMA2" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA2"
"NADD_MUL_LINV_LEMMA1" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA1"
"NADD_MUL_LINV_LEMMA0" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA0"
"NADD_MUL_LINV" > "HOLLight.hollight.NADD_MUL_LINV"
"NADD_MUL_LID" > "HOLLight.hollight.NADD_MUL_LID"
"NADD_MUL_ASSOC" > "HOLLight.hollight.NADD_MUL_ASSOC"
"NADD_MULTIPLICATIVE" > "HOLLight.hollight.NADD_MULTIPLICATIVE"
"NADD_MUL" > "HOLLight.hollight.NADD_MUL"
"NADD_LE_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_LE_WELLDEF_LEMMA"
"NADD_LE_WELLDEF" > "HOLLight.hollight.NADD_LE_WELLDEF"
"NADD_LE_TRANS" > "HOLLight.hollight.NADD_LE_TRANS"
"NADD_LE_TOTAL_LEMMA" > "HOLLight.hollight.NADD_LE_TOTAL_LEMMA"
"NADD_LE_TOTAL" > "HOLLight.hollight.NADD_LE_TOTAL"
"NADD_LE_RMUL" > "HOLLight.hollight.NADD_LE_RMUL"
"NADD_LE_REFL" > "HOLLight.hollight.NADD_LE_REFL"
"NADD_LE_RADD" > "HOLLight.hollight.NADD_LE_RADD"
"NADD_LE_LMUL" > "HOLLight.hollight.NADD_LE_LMUL"
"NADD_LE_LADD" > "HOLLight.hollight.NADD_LE_LADD"
"NADD_LE_EXISTS" > "HOLLight.hollight.NADD_LE_EXISTS"
"NADD_LE_ANTISYM" > "HOLLight.hollight.NADD_LE_ANTISYM"
"NADD_LE_ADD" > "HOLLight.hollight.NADD_LE_ADD"
"NADD_LE_0" > "HOLLight.hollight.NADD_LE_0"
"NADD_LDISTRIB" > "HOLLight.hollight.NADD_LDISTRIB"
"NADD_LBOUND" > "HOLLight.hollight.NADD_LBOUND"
"NADD_INV_WELLDEF" > "HOLLight.hollight.NADD_INV_WELLDEF"
"NADD_INV_0" > "HOLLight.hollight.NADD_INV_0"
"NADD_INV" > "HOLLight.hollight.NADD_INV"
"NADD_EQ_TRANS" > "HOLLight.hollight.NADD_EQ_TRANS"
"NADD_EQ_SYM" > "HOLLight.hollight.NADD_EQ_SYM"
"NADD_EQ_REFL" > "HOLLight.hollight.NADD_EQ_REFL"
"NADD_EQ_IMP_LE" > "HOLLight.hollight.NADD_EQ_IMP_LE"
"NADD_DIST_LEMMA" > "HOLLight.hollight.NADD_DIST_LEMMA"
"NADD_DIST" > "HOLLight.hollight.NADD_DIST"
"NADD_COMPLETE" > "HOLLight.hollight.NADD_COMPLETE"
"NADD_CAUCHY" > "HOLLight.hollight.NADD_CAUCHY"
"NADD_BOUND" > "HOLLight.hollight.NADD_BOUND"
"NADD_ARCH_ZERO" > "HOLLight.hollight.NADD_ARCH_ZERO"
"NADD_ARCH_MULT" > "HOLLight.hollight.NADD_ARCH_MULT"
"NADD_ARCH_LEMMA" > "HOLLight.hollight.NADD_ARCH_LEMMA"
"NADD_ARCH" > "HOLLight.hollight.NADD_ARCH"
"NADD_ALTMUL" > "HOLLight.hollight.NADD_ALTMUL"
"NADD_ADD_WELLDEF" > "HOLLight.hollight.NADD_ADD_WELLDEF"
"NADD_ADD_SYM" > "HOLLight.hollight.NADD_ADD_SYM"
"NADD_ADD_LID" > "HOLLight.hollight.NADD_ADD_LID"
"NADD_ADD_LCANCEL" > "HOLLight.hollight.NADD_ADD_LCANCEL"
"NADD_ADD_ASSOC" > "HOLLight.hollight.NADD_ADD_ASSOC"
"NADD_ADDITIVE" > "HOLLight.hollight.NADD_ADDITIVE"
"NADD_ADD" > "HOLLight.hollight.NADD_ADD"
"MULT_SYM" > "Fields.linordered_field_class.sign_simps_40"
"MULT_SUC" > "Nat.mult_Suc_right"
"MULT_EXP" > "Power.comm_monoid_mult_class.power_mult_distrib"
"MULT_EQ_1" > "Nat.nat_mult_eq_1_iff"
"MULT_EQ_0" > "Nat.mult_is_0"
"MULT_DIV_LE" > "HOLLight.hollight.MULT_DIV_LE"
"MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
"MULT_ASSOC" > "Fields.linordered_field_class.sign_simps_41"
"MULT_AC" > "HOLLight.hollight.MULT_AC"
"MULT_2" > "Int.semiring_mult_2"
"MULT_0" > "Divides.arithmetic_simps_41"
"MONO_FORALL" > "Inductive.basic_monos_6"
"MONO_EXISTS" > "Inductive.basic_monos_5"
"MONO_COND" > "HOLLight.hollight.MONO_COND"
"MONO_ALL2" > "List.list_all2_mono"
"MONO_ALL" > "HOLLightList.MONO_ALL"
"MONOIDAL_REAL_MUL" > "HOLLight.hollight.MONOIDAL_REAL_MUL"
"MONOIDAL_REAL_ADD" > "HOLLight.hollight.MONOIDAL_REAL_ADD"
"MONOIDAL_MUL" > "HOLLight.hollight.MONOIDAL_MUL"
"MONOIDAL_ADD" > "HOLLight.hollight.MONOIDAL_ADD"
"MONOIDAL_AC" > "HOLLight.hollight.MONOIDAL_AC"
"MOD_UNIQ" > "HOLLight.hollight.MOD_UNIQ"
"MOD_MULT_RMOD" > "HOLLight.hollight.MOD_MULT_RMOD"
"MOD_MULT_MOD2" > "HOLLight.hollight.MOD_MULT_MOD2"
"MOD_MULT_LMOD" > "HOLLight.hollight.MOD_MULT_LMOD"
"MOD_MULT_ADD" > "Divides.mod_mult_self3"
"MOD_MULT2" > "HOLLight.hollight.MOD_MULT2"
"MOD_MOD_REFL" > "HOLLight.hollight.MOD_MOD_REFL"
"MOD_MOD" > "HOLLight.hollight.MOD_MOD"
"MOD_LT" > "Divides.mod_less"
"MOD_LE" > "HOLLight.hollight.MOD_LE"
"MOD_EXP_MOD" > "HOLLight.hollight.MOD_EXP_MOD"
"MOD_EXISTS" > "HOLLight.hollight.MOD_EXISTS"
"MOD_EQ_0" > "HOLLight.hollight.MOD_EQ_0"
"MOD_EQ" > "HOLLight.hollight.MOD_EQ"
"MOD_ADD_MOD" > "HOLLight.hollight.MOD_ADD_MOD"
"MK_REC_INJ" > "HOLLight.hollight.MK_REC_INJ"
"MINIMAL" > "HOLLight.hollight.MINIMAL"
"MEM_MAP" > "HOLLightList.MEM_MAP"
"MEM_FILTER" > "HOLLightList.MEM_FILTER"
"MEM_EXISTS_EL" > "HOLLightList.MEM_EXISTS_EL"
"MEM_EL" > "List.nth_mem"
"MEM_APPEND" > "HOLLightList.MEM_APPEND"
"MEMBER_NOT_EMPTY" > "Set.ex_in_conv"
"MEASURE_LE" > "HOLLight.hollight.MEASURE_LE"
"MATCH_SEQPATTERN" > "HOLLight.hollight.MATCH_SEQPATTERN"
"MAP_o" > "List.map.compositionality"
"MAP_SND_ZIP" > "List.map_snd_zip"
"MAP_ID" > "List.map_ident"
"MAP_I" > "List.map.id"
"MAP_FST_ZIP" > "List.map_fst_zip"
"MAP_EQ_NIL" > "List.map_is_Nil_conv"
"MAP_EQ_DEGEN" > "HOLLightList.MAP_EQ_DEGEN"
"MAP_EQ_ALL2" > "HOLLightList.MAP_EQ_ALL2"
"MAP_EQ" > "HOLLightList.MAP_EQ"
"MAP_APPEND" > "List.map_append"
"MAP2" > "HOLLightList.MAP2"
"LT_TRANS" > "Orderings.order_less_trans"
"LT_SUC_LE" > "Nat.le_simps_2"
"LT_SUC" > "Nat.Suc_less_eq"
"LT_REFL" > "Nat.less_not_refl"
"LT_NZ" > "Nat.neq0_conv"
"LT_MULT_RCANCEL" > "HOLLight.hollight.LT_MULT_RCANCEL"
"LT_MULT_LCANCEL" > "HOLLight.hollight.LT_MULT_LCANCEL"
"LT_MULT2" > "HOLLight.hollight.LT_MULT2"
"LT_MULT" > "Nat.nat_0_less_mult_iff"
"LT_LMULT" > "HOLLight.hollight.LT_LMULT"
"LT_LE" > "Nat.nat_less_le"
"LT_IMP_LE" > "FunDef.termination_basic_simps_5"
"LT_EXP" > "HOLLight.hollight.LT_EXP"
"LT_EXISTS" > "HOLLight.hollight.LT_EXISTS"
"LT_CASES" > "HOLLight.hollight.LT_CASES"
"LT_ANTISYM" > "HOLLight.hollight.LT_ANTISYM"
"LT_ADD_RCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_right"
"LT_ADD_LCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_less_cancel_left"
"LT_ADDR" > "HOLLight.hollight.LT_ADDR"
"LT_ADD2" > "Groups.add_mono_thms_linordered_field_5"
"LT_ADD" > "HOLLight.hollight.LT_ADD"
"LT_0" > "Nat.zero_less_Suc"
"LTE_TRANS" > "Orderings.order_less_le_trans"
"LTE_CASES" > "HOLLight.hollight.LTE_CASES"
"LTE_ANTISYM" > "HOLLight.hollight.LTE_ANTISYM"
"LTE_ADD2" > "Groups.add_mono_thms_linordered_field_3"
"LE_TRANS" > "Nat.le_trans"
"LE_SUC_LT" > "Nat.Suc_le_eq"
"LE_SUC" > "Nat.Suc_le_mono"
"LE_SQUARE_REFL" > "Nat.le_square"
"LE_REFL" > "Nat.le_refl"
"LE_RDIV_EQ" > "HOLLight.hollight.LE_RDIV_EQ"
"LE_MULT_RCANCEL" > "HOLLight.hollight.LE_MULT_RCANCEL"
"LE_MULT_LCANCEL" > "HOLLight.hollight.LE_MULT_LCANCEL"
"LE_MULT2" > "Nat.mult_le_mono"
"LE_LT" > "Nat.le_eq_less_or_eq"
"LE_LDIV_EQ" > "HOLLight.hollight.LE_LDIV_EQ"
"LE_LDIV" > "HOLLight.hollight.LE_LDIV"
"LE_EXP" > "HOLLight.hollight.LE_EXP"
"LE_EXISTS" > "Nat.le_iff_add"
"LE_CASES" > "Nat.nat_le_linear"
"LE_C" > "HOLLight.hollight.LE_C"
"LE_ANTISYM" > "Orderings.order_class.eq_iff"
"LE_ADD_RCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_right"
"LE_ADD_LCANCEL" > "Groups.ordered_ab_semigroup_add_imp_le_class.add_le_cancel_left"
"LE_ADDR" > "Nat.le_add2"
"LE_ADD2" > "Groups.add_mono_thms_linordered_semiring_1"
"LE_ADD" > "Nat.le_add1"
"LE_1" > "HOLLight.hollight.LE_1"
"LE_0" > "Nat.le0"
"LET_TRANS" > "Orderings.order_le_less_trans"
"LET_END_def" > "HOLLight.hollight.LET_END_def"
"LET_CASES" > "Orderings.linorder_class.le_less_linear"
"LET_ANTISYM" > "HOLLight.hollight.LET_ANTISYM"
"LET_ADD2" > "Groups.add_mono_thms_linordered_field_4"
"LENGTH_TL" > "HOLLightList.LENGTH_TL"
"LENGTH_REPLICATE" > "List.length_replicate"
"LENGTH_MAP2" > "HOLLightList.LENGTH_MAP2"
"LENGTH_MAP" > "List.length_map"
"LENGTH_EQ_NIL" > "List.length_0_conv"
"LENGTH_EQ_CONS" > "List.length_Suc_conv"
"LENGTH_APPEND" > "List.length_append"
"LEFT_SUB_DISTRIB" > "Nat.diff_mult_distrib2"
"LEFT_OR_FORALL_THM" > "HOL.all_simps_3"
"LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
"LEFT_OR_DISTRIB" > "Groebner_Basis.dnf_1"
"LEFT_IMP_FORALL_THM" > "HOL.ex_simps_5"
"LEFT_IMP_EXISTS_THM" > "HOL.all_simps_5"
"LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
"LEFT_FORALL_IMP_THM" > "HOL.all_simps_5"
"LEFT_EXISTS_IMP_THM" > "HOL.ex_simps_5"
"LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
"LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
"LEFT_AND_EXISTS_THM" > "HOL.ex_simps_1"
"LEFT_ADD_DISTRIB" > "Fields.linordered_field_class.sign_simps_25"
"LAST_EL" > "List.last_conv_nth"
"LAST_CLAUSES" > "HOLLightList.LAST_CLAUSES"
"LAST_APPEND" > "List.last_append"
"LAMBDA_UNIQUE" > "HOLLight.hollight.LAMBDA_UNIQUE"
"LAMBDA_PAIR_THM" > "HOLLight.hollight.LAMBDA_PAIR_THM"
"LAMBDA_ETA" > "HOLLight.hollight.LAMBDA_ETA"
"LAMBDA_BETA" > "HOLLight.hollight.LAMBDA_BETA"
"I_THM" > "HOL.refl"
"I_O_ID" > "HOLLight.hollight.I_O_ID"
"ITSET_def" > "HOLLight.hollight.ITSET_def"
"ITSET_EQ" > "HOLLight.hollight.ITSET_EQ"
"ITLIST_EXTRA" > "HOLLightList.ITLIST_EXTRA"
"ITLIST_APPEND" > "List.foldr_append"
"ITLIST2" > "HOLLightList.ITLIST2"
"ITERATE_UNION_NONZERO" > "HOLLight.hollight.ITERATE_UNION_NONZERO"
"ITERATE_UNION_GEN" > "HOLLight.hollight.ITERATE_UNION_GEN"
"ITERATE_UNION" > "HOLLight.hollight.ITERATE_UNION"
"ITERATE_SUPPORT" > "HOLLight.hollight.ITERATE_SUPPORT"
"ITERATE_SUPERSET" > "HOLLight.hollight.ITERATE_SUPERSET"
"ITERATE_SING" > "HOLLight.hollight.ITERATE_SING"
"ITERATE_RELATED" > "HOLLight.hollight.ITERATE_RELATED"
"ITERATE_PAIR" > "HOLLight.hollight.ITERATE_PAIR"
"ITERATE_OP_GEN" > "HOLLight.hollight.ITERATE_OP_GEN"
"ITERATE_OP" > "HOLLight.hollight.ITERATE_OP"
"ITERATE_ITERATE_PRODUCT" > "HOLLight.hollight.ITERATE_ITERATE_PRODUCT"
"ITERATE_INJECTION" > "HOLLight.hollight.ITERATE_INJECTION"
"ITERATE_INCL_EXCL" > "HOLLight.hollight.ITERATE_INCL_EXCL"
"ITERATE_IMAGE_NONZERO" > "HOLLight.hollight.ITERATE_IMAGE_NONZERO"
"ITERATE_IMAGE" > "HOLLight.hollight.ITERATE_IMAGE"
"ITERATE_EXPAND_CASES" > "HOLLight.hollight.ITERATE_EXPAND_CASES"
"ITERATE_EQ_NEUTRAL" > "HOLLight.hollight.ITERATE_EQ_NEUTRAL"
"ITERATE_EQ_GENERAL_INVERSES" > "HOLLight.hollight.ITERATE_EQ_GENERAL_INVERSES"
"ITERATE_EQ_GENERAL" > "HOLLight.hollight.ITERATE_EQ_GENERAL"
"ITERATE_EQ" > "HOLLight.hollight.ITERATE_EQ"
"ITERATE_DIFF_GEN" > "HOLLight.hollight.ITERATE_DIFF_GEN"
"ITERATE_DIFF" > "HOLLight.hollight.ITERATE_DIFF"
"ITERATE_DELTA" > "HOLLight.hollight.ITERATE_DELTA"
"ITERATE_DELETE" > "HOLLight.hollight.ITERATE_DELETE"
"ITERATE_CLOSED" > "HOLLight.hollight.ITERATE_CLOSED"
"ITERATE_CLAUSES_NUMSEG" > "HOLLight.hollight.ITERATE_CLAUSES_NUMSEG"
"ITERATE_CLAUSES_GEN" > "HOLLight.hollight.ITERATE_CLAUSES_GEN"
"ITERATE_CLAUSES" > "HOLLight.hollight.ITERATE_CLAUSES"
"ITERATE_CASES" > "HOLLight.hollight.ITERATE_CASES"
"ITERATE_BIJECTION" > "HOLLight.hollight.ITERATE_BIJECTION"
"ISO_def" > "HOLLight.hollight.ISO_def"
"ISO_USAGE" > "HOLLight.hollight.ISO_USAGE"
"ISO_REFL" > "HOLLight.hollight.ISO_REFL"
"ISO_FUN" > "HOLLight.hollight.ISO_FUN"
"IN_UNIV" > "Set.UNIV_I"
"IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
"IN_UNION" > "Complete_Lattices.mem_simps_3"
"IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
"IN_SING" > "Set.singleton_iff"
"IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
"IN_REST" > "HOLLight.hollight.IN_REST"
"IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
"IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
"IN_INTERS" > "HOLLight.hollight.IN_INTERS"
"IN_INTER" > "Complete_Lattices.mem_simps_4"
"IN_INSERT" > "Complete_Lattices.mem_simps_1"
"IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
"IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
"IN_ELIM_PAIR_THM" > "HOLLight.hollight.IN_ELIM_PAIR_THM"
"IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
"IN_DIFF" > "Complete_Lattices.mem_simps_6"
"IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
"IN_DELETE" > "HOLLight.hollight.IN_DELETE"
"IN_CROSS" > "HOLLight.hollight.IN_CROSS"
"INT_WOP" > "HOLLight.hollight.INT_WOP"
"INT_POW" > "HOLLight.hollight.INT_POW"
"INT_OF_NUM_OF_INT" > "HOLLight.hollight.INT_OF_NUM_OF_INT"
"INT_LT_DISCRETE" > "HOLLight.hollight.INT_LT_DISCRETE"
"INT_LT" > "HOLLight.hollight.INT_LT"
"INT_INTEGRAL" > "HOLLight.hollight.INT_INTEGRAL"
"INT_IMAGE" > "HOLLight.hollight.INT_IMAGE"
"INT_GT_DISCRETE" > "HOLLight.hollight.INT_GT_DISCRETE"
"INT_GT" > "HOLLight.hollight.INT_GT"
"INT_GE" > "HOLLight.hollight.INT_GE"
"INT_GCD_EXISTS_POS" > "HOLLight.hollight.INT_GCD_EXISTS_POS"
"INT_GCD_EXISTS" > "HOLLight.hollight.INT_GCD_EXISTS"
"INT_FORALL_POS" > "HOLLight.hollight.INT_FORALL_POS"
"INT_FORALL_ABS" > "HOLLight.hollight.INT_FORALL_ABS"
"INT_EXISTS_POS" > "HOLLight.hollight.INT_EXISTS_POS"
"INT_EXISTS_ABS" > "HOLLight.hollight.INT_EXISTS_ABS"
"INT_DIVMOD_UNIQ" > "HOLLight.hollight.INT_DIVMOD_UNIQ"
"INT_DIVMOD_EXIST_0" > "HOLLight.hollight.INT_DIVMOD_EXIST_0"
"INT_DIVISION" > "HOLLight.hollight.INT_DIVISION"
"INT_ARCH" > "HOLLight.hollight.INT_ARCH"
"INT_ABS_MUL_1" > "HOLLight.hollight.INT_ABS_MUL_1"
"INT_ABS" > "HOLLight.hollight.INT_ABS"
"INTER_UNIV" > "HOLLight.hollight.INTER_UNIV"
"INTER_UNIONS" > "HOLLight.hollight.INTER_UNIONS"
"INTER_SUBSET" > "HOLLight.hollight.INTER_SUBSET"
"INTER_OVER_UNION" > "Lattices.distrib_lattice_class.distrib_1"
"INTER_IDEMPOT" > "Big_Operators.lattice_class.Inf_fin.idem"
"INTER_EMPTY" > "HOLLight.hollight.INTER_EMPTY"
"INTER_COMM" > "Lattices.lattice_class.inf_sup_aci_1"
"INTER_ASSOC" > "Lattices.lattice_class.inf_sup_aci_2"
"INTER_ACI" > "HOLLight.hollight.INTER_ACI"
"INTERS_UNIONS" > "HOLLight.hollight.INTERS_UNIONS"
"INTERS_INSERT" > "Complete_Lattices.Inter_insert"
"INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
"INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
"INTERS_2" > "Complete_Lattices.Int_eq_Inter"
"INTERS_1" > "Complete_Lattices.complete_lattice_class.Inf_singleton"
"INTERS_0" > "Complete_Lattices.Inter_empty"
"INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
"INSERT_UNION_EQ" > "Set.Un_insert_left"
"INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
"INSERT_SUBSET" > "Set.insert_subset"
"INSERT_INTER" > "Set.Int_insert_left"
"INSERT_INSERT" > "Set.insert_absorb2"
"INSERT_DIFF" > "Set.insert_Diff_if"
"INSERT_DELETE" > "Set.insert_Diff"
"INSERT_COMM" > "Set.insert_commute"
"INSERT_AC" > "HOLLight.hollight.INSERT_AC"
"INSERT" > "HOLLight.hollight.INSERT"
"INJ_def" > "HOLLight.hollight.INJ_def"
"INJ_INVERSE2" > "HOLLight.hollight.INJ_INVERSE2"
"INJP_def" > "HOLLight.hollight.INJP_def"
"INJP_INJ" > "HOLLight.hollight.INJP_INJ"
"INJN_def" > "HOLLight.hollight.INJN_def"
"INJN_INJ" > "HOLLight.hollight.INJN_INJ"
"INJF_def" > "HOLLight.hollight.INJF_def"
"INJF_INJ" > "HOLLight.hollight.INJF_INJ"
"INJECTIVE_ON_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_ON_LEFT_INVERSE"
"INJECTIVE_ON_IMAGE" > "HOLLight.hollight.INJECTIVE_ON_IMAGE"
"INJECTIVE_MAP" > "HOLLightList.INJECTIVE_MAP"
"INJECTIVE_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_LEFT_INVERSE"
"INJECTIVE_IMAGE" > "HOLLight.hollight.INJECTIVE_IMAGE"
"INJA_def" > "HOLLight.hollight.INJA_def"
"INJA_INJ" > "HOLLight.hollight.INJA_INJ"
"INFINITE_NONEMPTY" > "Infinite_Set.infinite_imp_nonempty"
"INFINITE_IMAGE_INJ" > "HOLLight.hollight.INFINITE_IMAGE_INJ"
"INFINITE_DIFF_FINITE" > "Infinite_Set.Diff_infinite_finite"
"IND_SUC_def" > "HOLLight.hollight.IND_SUC_def"
"IND_SUC_0_EXISTS" > "HOLLight.hollight.IND_SUC_0_EXISTS"
"IND_0_def" > "HOLLight.hollight.IND_0_def"
"IMP_EQ_CLAUSE" > "HOLLight.hollight.IMP_EQ_CLAUSE"
"IMP_CONJ_ALT" > "HOLLight.hollight.IMP_CONJ_ALT"
"IMP_CONJ" > "HOL.imp_conjL"
"IMP_CLAUSES" > "HOLLight.hollight.IMP_CLAUSES"
"IMAGE_o" > "Fun.image_compose"
"IMAGE_UNIONS" > "HOLLight.hollight.IMAGE_UNIONS"
"IMAGE_UNION" > "Set.image_Un"
"IMAGE_SUBSET" > "Set.image_mono"
"IMAGE_INTER_INJ" > "HOLLight.hollight.IMAGE_INTER_INJ"
"IMAGE_INJECTIVE_IMAGE_OF_SUBSET" > "HOLLight.hollight.IMAGE_INJECTIVE_IMAGE_OF_SUBSET"
"IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
"IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
"IMAGE_ID" > "Set.image_ident"
"IMAGE_I" > "Fun.image_id"
"IMAGE_EQ_EMPTY" > "Set.image_is_empty"
"IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
"IMAGE_DELETE_INJ" > "HOLLight.hollight.IMAGE_DELETE_INJ"
"IMAGE_CONST" > "Set.image_constant_conv"
"IMAGE_CLAUSES" > "HOLLight.hollight.IMAGE_CLAUSES"
"HREAL_MUL_RZERO" > "HOLLight.hollight.HREAL_MUL_RZERO"
"HREAL_MUL_LZERO" > "HOLLight.hollight.HREAL_MUL_LZERO"
"HREAL_LE_MUL_RCANCEL_IMP" > "HOLLight.hollight.HREAL_LE_MUL_RCANCEL_IMP"
"HREAL_LE_EXISTS_DEF" > "HOLLight.hollight.HREAL_LE_EXISTS_DEF"
"HREAL_LE_ADD_RCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_RCANCEL"
"HREAL_LE_ADD_LCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_LCANCEL"
"HREAL_LE_ADD2" > "HOLLight.hollight.HREAL_LE_ADD2"
"HREAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_RCANCEL"
"HREAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_LCANCEL"
"HREAL_ADD_RID" > "HOLLight.hollight.HREAL_ADD_RID"
"HREAL_ADD_RDISTRIB" > "HOLLight.hollight.HREAL_ADD_RDISTRIB"
"HREAL_ADD_AC" > "HOLLight.hollight.HREAL_ADD_AC"
"HD_APPEND" > "List.hd_append"
"HAS_SIZE_def" > "HOLLight.hollight.HAS_SIZE_def"
"HAS_SIZE_UNIONS" > "HOLLight.hollight.HAS_SIZE_UNIONS"
"HAS_SIZE_UNION" > "HOLLight.hollight.HAS_SIZE_UNION"
"HAS_SIZE_SUC" > "HOLLight.hollight.HAS_SIZE_SUC"
"HAS_SIZE_PRODUCT_DEPENDENT" > "HOLLight.hollight.HAS_SIZE_PRODUCT_DEPENDENT"
"HAS_SIZE_PRODUCT" > "HOLLight.hollight.HAS_SIZE_PRODUCT"
"HAS_SIZE_POWERSET" > "HOLLight.hollight.HAS_SIZE_POWERSET"
"HAS_SIZE_NUMSEG_LT" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LT"
"HAS_SIZE_NUMSEG_LE" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LE"
"HAS_SIZE_NUMSEG_1" > "HOLLight.hollight.HAS_SIZE_NUMSEG_1"
"HAS_SIZE_NUMSEG" > "HOLLight.hollight.HAS_SIZE_NUMSEG"
"HAS_SIZE_INDEX" > "HOLLight.hollight.HAS_SIZE_INDEX"
"HAS_SIZE_IMAGE_INJ_EQ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ_EQ"
"HAS_SIZE_IMAGE_INJ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ"
"HAS_SIZE_FUNSPACE" > "HOLLight.hollight.HAS_SIZE_FUNSPACE"
"HAS_SIZE_FINITE_IMAGE" > "HOLLight.hollight.HAS_SIZE_FINITE_IMAGE"
"HAS_SIZE_DIFF" > "HOLLight.hollight.HAS_SIZE_DIFF"
"HAS_SIZE_CROSS" > "HOLLight.hollight.HAS_SIZE_CROSS"
"HAS_SIZE_CLAUSES" > "HOLLight.hollight.HAS_SIZE_CLAUSES"
"HAS_SIZE_CARD" > "HOLLight.hollight.HAS_SIZE_CARD"
"HAS_SIZE_1" > "HOLLight.hollight.HAS_SIZE_1"
"HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
"GE_C" > "HOLLight.hollight.GE_C"
"FUN_IN_IMAGE" > "Set.imageI"
"FUN_EQ_THM" > "HOL.fun_eq_iff"
"FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
"FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
"FST" > "Product_Type.fst_conv"
"FORALL_UNWIND_THM2" > "HOL.simp_thms_41"
"FORALL_UNWIND_THM1" > "HOL.simp_thms_42"
"FORALL_UNCURRY" > "HOLLight.hollight.FORALL_UNCURRY"
"FORALL_TRIPLED_THM" > "HOLLight.hollight.FORALL_TRIPLED_THM"
"FORALL_SUBSET_IMAGE" > "HOLLight.hollight.FORALL_SUBSET_IMAGE"
"FORALL_SIMP" > "HOL.simp_thms_35"
"FORALL_PAIR_THM" > "Product_Type.split_paired_All"
"FORALL_PAIRED_THM" > "HOLLight.hollight.FORALL_PAIRED_THM"
"FORALL_NOT_THM" > "HOL.not_ex"
"FORALL_IN_UNIONS" > "HOLLight.hollight.FORALL_IN_UNIONS"
"FORALL_IN_INSERT" > "HOLLight.hollight.FORALL_IN_INSERT"
"FORALL_IN_IMAGE" > "HOLLight.hollight.FORALL_IN_IMAGE"
"FORALL_IN_GSPEC" > "HOLLight.hollight.FORALL_IN_GSPEC"
"FORALL_IN_CLAUSES" > "HOLLight.hollight.FORALL_IN_CLAUSES"
"FORALL_FINITE_INDEX" > "HOLLight.hollight.FORALL_FINITE_INDEX"
"FORALL_BOOL_THM" > "Set.all_bool_eq"
"FORALL_AND_THM" > "HOL.all_conj_distrib"
"FORALL_ALL" > "HOLLightList.FORALL_ALL"
"FNIL_def" > "HOLLight.hollight.FNIL_def"
"FINREC_def" > "HOLLight.hollight.FINREC_def"
"FINREC_UNIQUE_LEMMA" > "HOLLight.hollight.FINREC_UNIQUE_LEMMA"
"FINREC_SUC_LEMMA" > "HOLLight.hollight.FINREC_SUC_LEMMA"
"FINREC_FUN_LEMMA" > "HOLLight.hollight.FINREC_FUN_LEMMA"
"FINREC_FUN" > "HOLLight.hollight.FINREC_FUN"
"FINREC_EXISTS_LEMMA" > "HOLLight.hollight.FINREC_EXISTS_LEMMA"
"FINREC_1_LEMMA" > "HOLLight.hollight.FINREC_1_LEMMA"
"FINITE_UNION_IMP" > "Finite_Set.finite_UnI"
"FINITE_UNIONS" > "HOLLight.hollight.FINITE_UNIONS"
"FINITE_UNION" > "Finite_Set.finite_Un"
"FINITE_SUPPORT_DELTA" > "HOLLight.hollight.FINITE_SUPPORT_DELTA"
"FINITE_SUPPORT" > "HOLLight.hollight.FINITE_SUPPORT"
"FINITE_SUM_IMAGE" > "HOLLight.hollight.FINITE_SUM_IMAGE"
"FINITE_SUBSET_IMAGE_IMP" > "HOLLight.hollight.FINITE_SUBSET_IMAGE_IMP"
"FINITE_SUBSET_IMAGE" > "HOLLight.hollight.FINITE_SUBSET_IMAGE"
"FINITE_SUBSET" > "Finite_Set.finite_subset"
"FINITE_SING" > "HOLLight.hollight.FINITE_SING"
"FINITE_RESTRICT" > "HOLLight.hollight.FINITE_RESTRICT"
"FINITE_RECURSION_DELETE" > "HOLLight.hollight.FINITE_RECURSION_DELETE"
"FINITE_RECURSION" > "HOLLight.hollight.FINITE_RECURSION"
"FINITE_REAL_INTERVAL" > "HOLLight.hollight.FINITE_REAL_INTERVAL"
"FINITE_PRODUCT_DEPENDENT" > "HOLLight.hollight.FINITE_PRODUCT_DEPENDENT"
"FINITE_PRODUCT" > "HOLLight.hollight.FINITE_PRODUCT"
"FINITE_POWERSET" > "HOLLight.hollight.FINITE_POWERSET"
"FINITE_NUMSEG_LT" > "HOLLight.hollight.FINITE_NUMSEG_LT"
"FINITE_NUMSEG_LE" > "HOLLight.hollight.FINITE_NUMSEG_LE"
"FINITE_NUMSEG" > "SetInterval.finite_atLeastAtMost"
"FINITE_INTSEG" > "HOLLight.hollight.FINITE_INTSEG"
"FINITE_INTER" > "Finite_Set.finite_Int"
"FINITE_INSERT" > "Finite_Set.finite_insert"
"FINITE_INDUCT_STRONG" > "Finite_Set.finite_induct"
"FINITE_INDUCT_DELETE" > "HOLLight.hollight.FINITE_INDUCT_DELETE"
"FINITE_INDEX_WORKS" > "HOLLight.hollight.FINITE_INDEX_WORKS"
"FINITE_INDEX_NUMSEG" > "HOLLight.hollight.FINITE_INDEX_NUMSEG"
"FINITE_INDEX_NUMBERS" > "HOLLight.hollight.FINITE_INDEX_NUMBERS"
"FINITE_INDEX_INRANGE" > "HOLLight.hollight.FINITE_INDEX_INRANGE"
"FINITE_INDEX_INJ" > "HOLLight.hollight.FINITE_INDEX_INJ"
"FINITE_IMAGE_INJ_GENERAL" > "HOLLight.hollight.FINITE_IMAGE_INJ_GENERAL"
"FINITE_IMAGE_INJ_EQ" > "HOLLight.hollight.FINITE_IMAGE_INJ_EQ"
"FINITE_IMAGE_INJ" > "HOLLight.hollight.FINITE_IMAGE_INJ"
"FINITE_IMAGE_IMAGE" > "HOLLight.hollight.FINITE_IMAGE_IMAGE"
"FINITE_IMAGE_EXPAND" > "HOLLight.hollight.FINITE_IMAGE_EXPAND"
"FINITE_IMAGE" > "Finite_Set.finite_imageI"
"FINITE_HAS_SIZE" > "HOLLight.hollight.FINITE_HAS_SIZE"
"FINITE_FUNSPACE" > "HOLLight.hollight.FINITE_FUNSPACE"
"FINITE_FINITE_UNIONS" > "HOLLight.hollight.FINITE_FINITE_UNIONS"
"FINITE_FINITE_PREIMAGE_GENERAL" > "HOLLight.hollight.FINITE_FINITE_PREIMAGE_GENERAL"
"FINITE_FINITE_PREIMAGE" > "HOLLight.hollight.FINITE_FINITE_PREIMAGE"
"FINITE_FINITE_IMAGE" > "HOLLight.hollight.FINITE_FINITE_IMAGE"
"FINITE_EMPTY" > "Finite_Set.finite.emptyI"
"FINITE_DIFF" > "Finite_Set.finite_Diff"
"FINITE_DELETE_IMP" > "HOLLight.hollight.FINITE_DELETE_IMP"
"FINITE_DELETE" > "HOLLight.hollight.FINITE_DELETE"
"FINITE_CROSS" > "HOLLight.hollight.FINITE_CROSS"
"FINITE_CART" > "HOLLight.hollight.FINITE_CART"
"FILTER_MAP" > "List.filter_map"
"FILTER_APPEND" > "List.filter_append"
"FCONS_def" > "HOLLight.hollight.FCONS_def"
"FCONS_UNDO" > "HOLLight.hollight.FCONS_UNDO"
"FACT_NZ" > "Fact.fact_nonzero_nat"
"FACT_MONO" > "Fact.fact_mono_nat"
"FACT_LT" > "Fact.fact_gt_zero_nat"
"FACT_LE" > "Fact.fact_ge_one_nat"
"EX_MEM" > "HOLLightList.EX_MEM"
"EX_IMP" > "HOLLightList.EX_IMP"
"EXTENSION" > "Set.set_eq_iff"
"EXP_ZERO" > "Power.power_0_left"
"EXP_ONE" > "Power.monoid_mult_class.power_one"
"EXP_MULT" > "Power.monoid_mult_class.power_mult"
"EXP_MONO_LT_IMP" > "HOLLight.hollight.EXP_MONO_LT_IMP"
"EXP_MONO_LT" > "HOLLight.hollight.EXP_MONO_LT"
"EXP_MONO_LE_IMP" > "HOLLight.hollight.EXP_MONO_LE_IMP"
"EXP_MONO_LE" > "HOLLight.hollight.EXP_MONO_LE"
"EXP_MONO_EQ" > "HOLLight.hollight.EXP_MONO_EQ"
"EXP_LT_0" > "HOLLight.hollight.EXP_LT_0"
"EXP_EQ_1" > "HOLLight.hollight.EXP_EQ_1"
"EXP_EQ_0" > "Power.power_eq_0_iff"
"EXP_ADD" > "Power.monoid_mult_class.power_add"
"EXP_2" > "Nat_Numeral.monoid_mult_class.power2_eq_square"
"EXP_1" > "Power.monoid_mult_class.power_one_right"
"EXISTS_UNIQUE_THM" > "HOLLightCompat.EXISTS_UNIQUE_THM"
"EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
"EXISTS_UNIQUE_ALT" > "HOLLight.hollight.EXISTS_UNIQUE_ALT"
"EXISTS_UNIQUE" > "HOL.Ex1_def"
"EXISTS_UNCURRY" > "HOLLight.hollight.EXISTS_UNCURRY"
"EXISTS_TRIPLED_THM" > "HOLLight.hollight.EXISTS_TRIPLED_THM"
"EXISTS_THM" > "HOL4Setup.EXISTS_DEF"
"EXISTS_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_SUBSET_IMAGE"
"EXISTS_SIMP" > "HOL.simp_thms_36"
"EXISTS_REFL" > "HOL.simp_thms_37"
"EXISTS_PAIR_THM" > "Product_Type.split_paired_Ex"
"EXISTS_PAIRED_THM" > "HOLLight.hollight.EXISTS_PAIRED_THM"
"EXISTS_OR_THM" > "HOL.ex_disj_distrib"
"EXISTS_ONE_REP" > "HOLLight.hollight.EXISTS_ONE_REP"
"EXISTS_NOT_THM" > "HOL.not_all"
"EXISTS_IN_UNIONS" > "HOLLight.hollight.EXISTS_IN_UNIONS"
"EXISTS_IN_INSERT" > "HOLLight.hollight.EXISTS_IN_INSERT"
"EXISTS_IN_IMAGE" > "HOLLight.hollight.EXISTS_IN_IMAGE"
"EXISTS_IN_GSPEC" > "HOLLight.hollight.EXISTS_IN_GSPEC"
"EXISTS_IN_CLAUSES" > "HOLLight.hollight.EXISTS_IN_CLAUSES"
"EXISTS_FINITE_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_FINITE_SUBSET_IMAGE"
"EXISTS_EX" > "HOLLightList.EXISTS_EX"
"EXISTS_BOOL_THM" > "Set.ex_bool_eq"
"EXCLUDED_MIDDLE" > "HOLLight.hollight.EXCLUDED_MIDDLE"
"EVEN_SUB" > "HOLLight.hollight.EVEN_SUB"
"EVEN_OR_ODD" > "HOLLight.hollight.EVEN_OR_ODD"
"EVEN_ODD_DECOMPOSITION" > "HOLLight.hollight.EVEN_ODD_DECOMPOSITION"
"EVEN_MULT" > "Parity.even_product_nat"
"EVEN_MOD" > "HOLLight.hollight.EVEN_MOD"
"EVEN_EXP" > "HOLLight.hollight.EVEN_EXP"
"EVEN_EXISTS_LEMMA" > "HOLLight.hollight.EVEN_EXISTS_LEMMA"
"EVEN_EXISTS" > "Parity.even_mult_two_ex"
"EVEN_DOUBLE" > "HOLLight.hollight.EVEN_DOUBLE"
"EVEN_AND_ODD" > "HOLLight.hollight.EVEN_AND_ODD"
"EVEN_ADD" > "Parity.even_add"
"EQ_UNIV" > "HOLLight.hollight.EQ_UNIV"
"EQ_TRANS" > "HOL.trans"
"EQ_SYM_EQ" > "HOL.eq_ac_1"
"EQ_SYM" > "HOL.eq_reflection"
"EQ_REFL" > "HOL.refl"
"EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
"EQ_MULT_LCANCEL" > "Numeral_Simprocs.nat_mult_eq_cancel_disj"
"EQ_IMP_LE" > "Nat.eq_imp_le"
"EQ_EXT" > "HOL.eq_reflection"
"EQ_EXP" > "HOLLight.hollight.EQ_EXP"
"EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
"EQ_ADD_RCANCEL_0" > "HOLLight.hollight.EQ_ADD_RCANCEL_0"
"EQ_ADD_RCANCEL" > "Groups.cancel_semigroup_add_class.add_right_cancel"
"EQ_ADD_LCANCEL_0" > "HOLLight.hollight.EQ_ADD_LCANCEL_0"
"EQ_ADD_LCANCEL" > "Groups.cancel_semigroup_add_class.add_left_cancel"
"EMPTY_UNIONS" > "HOLLight.hollight.EMPTY_UNIONS"
"EMPTY_UNION" > "Lattices.bounded_lattice_bot_class.sup_eq_bot_iff"
"EMPTY_SUBSET" > "Orderings.bot_class.bot_least"
"EMPTY_NOT_UNIV" > "HOLLight.hollight.EMPTY_NOT_UNIV"
"EMPTY_GSPEC" > "HOLLight.hollight.EMPTY_GSPEC"
"EMPTY_DIFF" > "Set.empty_Diff"
"EMPTY_DELETE" > "HOLLight.hollight.EMPTY_DELETE"
"EL_CONS" > "List.nth_Cons'"
"EL_APPEND" > "List.nth_append"
"DIV_UNIQ" > "HOLLight.hollight.DIV_UNIQ"
"DIV_REFL" > "Divides.semiring_div_class.div_self"
"DIV_MUL_LE" > "HOLLight.hollight.DIV_MUL_LE"
"DIV_MULT2" > "HOLLight.hollight.DIV_MULT2"
"DIV_MONO_LT" > "HOLLight.hollight.DIV_MONO_LT"
"DIV_MONO2" > "HOLLight.hollight.DIV_MONO2"
"DIV_MONO" > "HOLLight.hollight.DIV_MONO"
"DIV_MOD" > "HOLLight.hollight.DIV_MOD"
"DIV_LT" > "Divides.div_less"
"DIV_LE_EXCLUSION" > "HOLLight.hollight.DIV_LE_EXCLUSION"
"DIV_LE" > "HOLLight.hollight.DIV_LE"
"DIV_EQ_EXCLUSION" > "HOLLight.hollight.DIV_EQ_EXCLUSION"
"DIV_EQ_0" > "HOLLight.hollight.DIV_EQ_0"
"DIV_DIV" > "HOLLight.hollight.DIV_DIV"
"DIV_ADD_MOD" > "HOLLight.hollight.DIV_ADD_MOD"
"DIVMOD_UNIQ_LEMMA" > "HOLLight.hollight.DIVMOD_UNIQ_LEMMA"
"DIVMOD_UNIQ" > "HOLLight.hollight.DIVMOD_UNIQ"
"DIVMOD_EXIST_0" > "HOLLight.hollight.DIVMOD_EXIST_0"
"DIVMOD_EXIST" > "HOLLight.hollight.DIVMOD_EXIST"
"DIVMOD_ELIM_THM" > "HOLLight.hollight.DIVMOD_ELIM_THM"
"DIVISION" > "HOLLight.hollight.DIVISION"
"DIST_TRIANGLE_LE" > "HOLLight.hollight.DIST_TRIANGLE_LE"
"DIST_TRIANGLES_LE" > "HOLLight.hollight.DIST_TRIANGLES_LE"
"DIST_SYM" > "HOLLight.hollight.DIST_SYM"
"DIST_RZERO" > "HOLLight.hollight.DIST_RZERO"
"DIST_RMUL" > "HOLLight.hollight.DIST_RMUL"
"DIST_REFL" > "HOLLight.hollight.DIST_REFL"
"DIST_RADD_0" > "HOLLight.hollight.DIST_RADD_0"
"DIST_RADD" > "HOLLight.hollight.DIST_RADD"
"DIST_LZERO" > "HOLLight.hollight.DIST_LZERO"
"DIST_LMUL" > "HOLLight.hollight.DIST_LMUL"
"DIST_LE_CASES" > "HOLLight.hollight.DIST_LE_CASES"
"DIST_LADD_0" > "HOLLight.hollight.DIST_LADD_0"
"DIST_LADD" > "HOLLight.hollight.DIST_LADD"
"DIST_EQ_0" > "HOLLight.hollight.DIST_EQ_0"
"DIST_ELIM_THM" > "HOLLight.hollight.DIST_ELIM_THM"
"DISJ_SYM" > "Groebner_Basis.dnf_4"
"DISJ_ASSOC" > "HOL.disj_ac_3"
"DISJ_ACI" > "HOLLight.hollight.DISJ_ACI"
"DISJOINT_UNION" > "HOLLight.hollight.DISJOINT_UNION"
"DISJOINT_SYM" > "HOLLight.hollight.DISJOINT_SYM"
"DISJOINT_NUMSEG" > "HOLLight.hollight.DISJOINT_NUMSEG"
"DISJOINT_INSERT" > "HOLLight.hollight.DISJOINT_INSERT"
"DISJOINT_EMPTY_REFL" > "HOLLight.hollight.DISJOINT_EMPTY_REFL"
"DISJOINT_EMPTY" > "HOLLight.hollight.DISJOINT_EMPTY"
"DISJOINT_DELETE_SYM" > "HOLLight.hollight.DISJOINT_DELETE_SYM"
"DIMINDEX_UNIV" > "HOLLight.hollight.DIMINDEX_UNIV"
"DIMINDEX_UNIQUE" > "HOLLight.hollight.DIMINDEX_UNIQUE"
"DIMINDEX_NONZERO" > "HOLLight.hollight.DIMINDEX_NONZERO"
"DIMINDEX_GE_1" > "HOLLight.hollight.DIMINDEX_GE_1"
"DIMINDEX_FINITE_IMAGE" > "HOLLight.hollight.DIMINDEX_FINITE_IMAGE"
"DIFF_UNIV" > "Set.Diff_UNIV"
"DIFF_INTERS" > "HOLLight.hollight.DIFF_INTERS"
"DIFF_INSERT" > "Set.Diff_insert2"
"DIFF_EQ_EMPTY" > "Set.Diff_cancel"
"DIFF_EMPTY" > "Set.Diff_empty"
"DIFF_DIFF" > "Set.Diff_idemp"
"DEST_REC_INJ" > "HOLLight.hollight.recspace._dest_rec_inject"
"DELETE_SUBSET" > "HOLLight.hollight.DELETE_SUBSET"
"DELETE_NON_ELEMENT" > "HOLLight.hollight.DELETE_NON_ELEMENT"
"DELETE_INTER" > "HOLLight.hollight.DELETE_INTER"
"DELETE_INSERT" > "HOLLight.hollight.DELETE_INSERT"
"DELETE_DELETE" > "HOLLight.hollight.DELETE_DELETE"
"DELETE_COMM" > "HOLLight.hollight.DELETE_COMM"
"DEF_~" > "Groebner_Basis.bool_simps_19"
"DEF_vector" > "HOLLight.hollight.DEF_vector"
"DEF_treal_of_num" > "HOLLight.hollight.DEF_treal_of_num"
"DEF_treal_neg" > "HOLLight.hollight.DEF_treal_neg"
"DEF_treal_mul" > "HOLLight.hollight.DEF_treal_mul"
"DEF_treal_le" > "HOLLight.hollight.DEF_treal_le"
"DEF_treal_inv" > "HOLLight.hollight.DEF_treal_inv"
"DEF_treal_eq" > "HOLLight.hollight.DEF_treal_eq"
"DEF_treal_add" > "HOLLight.hollight.DEF_treal_add"
"DEF_tailadmissible" > "HOLLight.hollight.DEF_tailadmissible"
"DEF_support" > "HOLLight.hollight.DEF_support"
"DEF_superadmissible" > "HOLLight.hollight.DEF_superadmissible"
"DEF_sum" > "HOLLight.hollight.DEF_sum"
"DEF_sndcart" > "HOLLight.hollight.DEF_sndcart"
"DEF_set_of_list" > "HOLLightList.DEF_set_of_list"
"DEF_rem" > "HOLLight.hollight.DEF_rem"
"DEF_real_sub" > "HOLLight.hollight.DEF_real_sub"
"DEF_real_sgn" > "HOLLight.hollight.DEF_real_sgn"
"DEF_real_pow" > "HOLLight.hollight.DEF_real_pow"
"DEF_real_of_num" > "HOLLight.hollight.DEF_real_of_num"
"DEF_real_neg" > "HOLLight.hollight.DEF_real_neg"
"DEF_real_mul" > "HOLLight.hollight.DEF_real_mul"
"DEF_real_mod" > "HOLLight.hollight.DEF_real_mod"
"DEF_real_min" > "HOLLight.hollight.DEF_real_min"
"DEF_real_max" > "HOLLight.hollight.DEF_real_max"
"DEF_real_lt" > "HOLLight.hollight.DEF_real_lt"
"DEF_real_le" > "HOLLight.hollight.DEF_real_le"
"DEF_real_inv" > "HOLLight.hollight.DEF_real_inv"
"DEF_real_gt" > "HOLLight.hollight.DEF_real_gt"
"DEF_real_ge" > "HOLLight.hollight.DEF_real_ge"
"DEF_real_div" > "HOLLight.hollight.DEF_real_div"
"DEF_real_add" > "HOLLight.hollight.DEF_real_add"
"DEF_real_abs" > "HOLLight.hollight.DEF_real_abs"
"DEF_pastecart" > "HOLLight.hollight.DEF_pastecart"
"DEF_pairwise" > "HOLLight.hollight.DEF_pairwise"
"DEF_o" > "Fun.comp_def"
"DEF_num_of_int" > "HOLLight.hollight.DEF_num_of_int"
"DEF_num_mod" > "HOLLight.hollight.DEF_num_mod"
"DEF_num_gcd" > "HOLLight.hollight.DEF_num_gcd"
"DEF_num_divides" > "HOLLight.hollight.DEF_num_divides"
"DEF_num_coprime" > "HOLLight.hollight.DEF_num_coprime"
"DEF_nsum" > "HOLLight.hollight.DEF_nsum"
"DEF_neutral" > "HOLLight.hollight.DEF_neutral"
"DEF_nadd_rinv" > "HOLLight.hollight.DEF_nadd_rinv"
"DEF_nadd_of_num" > "HOLLight.hollight.DEF_nadd_of_num"
"DEF_nadd_mul" > "HOLLight.hollight.DEF_nadd_mul"
"DEF_nadd_le" > "HOLLight.hollight.DEF_nadd_le"
"DEF_nadd_inv" > "HOLLight.hollight.DEF_nadd_inv"
"DEF_nadd_eq" > "HOLLight.hollight.DEF_nadd_eq"
"DEF_nadd_add" > "HOLLight.hollight.DEF_nadd_add"
"DEF_monoidal" > "HOLLight.hollight.DEF_monoidal"
"DEF_minimal" > "HOLLight.hollight.DEF_minimal"
"DEF_lambda" > "HOLLight.hollight.DEF_lambda"
"DEF_iterate" > "HOLLight.hollight.DEF_iterate"
"DEF_is_nadd" > "HOLLight.hollight.DEF_is_nadd"
"DEF_integer" > "HOLLight.hollight.DEF_integer"
"DEF_int_sub" > "HOLLight.hollight.DEF_int_sub"
"DEF_int_sgn" > "HOLLight.hollight.DEF_int_sgn"
"DEF_int_pow" > "HOLLight.hollight.DEF_int_pow"
"DEF_int_of_num" > "HOLLight.hollight.DEF_int_of_num"
"DEF_int_neg" > "HOLLight.hollight.DEF_int_neg"
"DEF_int_mul" > "HOLLight.hollight.DEF_int_mul"
"DEF_int_mod" > "HOLLight.hollight.DEF_int_mod"
"DEF_int_min" > "HOLLight.hollight.DEF_int_min"
"DEF_int_max" > "HOLLight.hollight.DEF_int_max"
"DEF_int_lt" > "HOLLight.hollight.DEF_int_lt"
"DEF_int_le" > "HOLLight.hollight.DEF_int_le"
"DEF_int_gt" > "HOLLight.hollight.DEF_int_gt"
"DEF_int_ge" > "HOLLight.hollight.DEF_int_ge"
"DEF_int_gcd" > "HOLLight.hollight.DEF_int_gcd"
"DEF_int_divides" > "HOLLight.hollight.DEF_int_divides"
"DEF_int_coprime" > "HOLLight.hollight.DEF_int_coprime"
"DEF_int_add" > "HOLLight.hollight.DEF_int_add"
"DEF_int_abs" > "HOLLight.hollight.DEF_int_abs"
"DEF_hreal_of_num" > "HOLLight.hollight.DEF_hreal_of_num"
"DEF_hreal_mul" > "HOLLight.hollight.DEF_hreal_mul"
"DEF_hreal_le" > "HOLLight.hollight.DEF_hreal_le"
"DEF_hreal_inv" > "HOLLight.hollight.DEF_hreal_inv"
"DEF_hreal_add" > "HOLLight.hollight.DEF_hreal_add"
"DEF_fstcart" > "HOLLight.hollight.DEF_fstcart"
"DEF_div" > "HOLLight.hollight.DEF_div"
"DEF_dist" > "HOLLight.hollight.DEF_dist"
"DEF_dimindex" > "HOLLight.hollight.DEF_dimindex"
"DEF_admissible" > "HOLLight.hollight.DEF_admissible"
"DEF__star_" > "HOLLightCompat.DEF__star_"
"DEF__slash__backslash_" > "HOLLightCompat.DEF__slash__backslash_"
"DEF__questionmark__exclamationmark_" > "HOLLightCompat.EXISTS_UNIQUE_THM"
"DEF__questionmark_" > "HOL.Ex_def"
"DEF__lessthan__equal__c" > "HOLLight.hollight.DEF__lessthan__equal__c"
"DEF__lessthan__equal_" > "HOLLightCompat.DEF__lessthan__equal_"
"DEF__lessthan__c" > "HOLLight.hollight.DEF__lessthan__c"
"DEF__lessthan_" > "HOLLightCompat.DEF__lessthan_"
"DEF__greaterthan__equal__c" > "HOLLight.hollight.DEF__greaterthan__equal__c"
"DEF__greaterthan__equal_" > "HOLLightCompat.DEF__greaterthan__equal_"
"DEF__greaterthan__c" > "HOLLight.hollight.DEF__greaterthan__c"
"DEF__greaterthan_" > "HOLLightCompat.DEF__greaterthan_"
"DEF__exclamationmark_" > "HOL.All_def"
"DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_"
"DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
"DEF__equal__c" > "HOLLight.hollight.DEF__equal__c"
"DEF__dot__dot_" > "HOLLightCompat.dotdot_def"
"DEF__backslash__slash_" > "HOL.or_def"
"DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN"
"DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN"
"DEF__MATCH" > "HOLLight.hollight.DEF__MATCH"
"DEF__GUARDED_PATTERN" > "HOLLight.hollight.DEF__GUARDED_PATTERN"
"DEF__FUNCTION" > "HOLLight.hollight.DEF__FUNCTION"
"DEF__FALSITY_" > "HOLLight.hollight.DEF__FALSITY_"
"DEF__11937" > "HOLLight.hollight.DEF__11937"
"DEF_ZRECSPACE" > "HOLLight.hollight.DEF_ZRECSPACE"
"DEF_ZCONSTR" > "HOLLight.hollight.DEF_ZCONSTR"
"DEF_ZBOT" > "HOLLight.hollight.DEF_ZBOT"
"DEF_WF" > "HOLLightCompat.DEF_WF"
"DEF_UNIV" > "HOLLightCompat.DEF_UNIV"
"DEF_UNIONS" > "HOLLightCompat.DEF_UNIONS"
"DEF_UNION" > "HOLLightCompat.DEF_UNION"
"DEF_UNCURRY" > "HOLLight.hollight.DEF_UNCURRY"
"DEF_T" > "HOL.True_def"
"DEF_SURJ" > "HOLLight.hollight.DEF_SURJ"
"DEF_SUBSET" > "HOLLightCompat.DEF_SUBSET"
"DEF_SND" > "HOLLightCompat.DEF_SND"
"DEF_SING" > "HOLLight.hollight.DEF_SING"
"DEF_SETSPEC" > "HOLLightCompat.SETSPEC_def"
"DEF_REVERSE" > "HOLLightList.DEF_REVERSE"
"DEF_REST" > "HOLLight.hollight.DEF_REST"
"DEF_REPLICATE" > "HOLLightList.DEF_REPLICATE"
"DEF_PSUBSET" > "HOLLightCompat.DEF_PSUBSET"
"DEF_PRE" > "HOLLightCompat.DEF_PRE"
"DEF_PASSOC" > "HOLLight.hollight.DEF_PASSOC"
"DEF_PAIRWISE" > "HOLLight.hollight.DEF_PAIRWISE"
"DEF_ONTO" > "Fun.surj_def"
"DEF_ONE_ONE" > "HOLLightCompat.DEF_ONE_ONE"
"DEF_ODD" > "HOLLightCompat.DEF_ODD"
"DEF_NUM_REP" > "HOLLight.hollight.DEF_NUM_REP"
"DEF_NUMSUM" > "HOLLight.hollight.DEF_NUMSUM"
"DEF_NUMSND" > "HOLLight.hollight.DEF_NUMSND"
"DEF_NUMRIGHT" > "HOLLight.hollight.DEF_NUMRIGHT"
"DEF_NUMPAIR" > "HOLLight.hollight.DEF_NUMPAIR"
"DEF_NUMLEFT" > "HOLLight.hollight.DEF_NUMLEFT"
"DEF_NUMFST" > "HOLLight.hollight.DEF_NUMFST"
"DEF_NUMERAL" > "HOLLightCompat.NUMERAL_def"
"DEF_NULL" > "HOLLightList.DEF_NULL"
"DEF_MOD" > "HOLLightCompat.DEF_MOD"
"DEF_MIN" > "Orderings.ord_class.min_def"
"DEF_MEM" > "HOLLightList.DEF_MEM"
"DEF_MEASURE" > "HOLLightCompat.MEASURE_def"
"DEF_MAX" > "Orderings.ord_class.max_def"
"DEF_MAP" > "HOLLightList.DEF_MAP"
"DEF_LET_END" > "HOLLight.hollight.DEF_LET_END"
"DEF_LET" > "HOLLightCompat.LET_def"
"DEF_LENGTH" > "HOLLightList.DEF_LENGTH"
"DEF_LAST" > "HOLLightList.DEF_LAST"
"DEF_ITSET" > "HOLLight.hollight.DEF_ITSET"
"DEF_ITLIST" > "HOLLightList.DEF_ITLIST"
"DEF_ISO" > "HOLLight.hollight.DEF_ISO"
"DEF_INTERS" > "HOLLightCompat.DEF_INTERS"
"DEF_INTER" > "HOLLightCompat.DEF_INTER"
"DEF_INSERT" > "HOLLightCompat.DEF_INSERT"
"DEF_INJP" > "HOLLight.hollight.DEF_INJP"
"DEF_INJN" > "HOLLight.hollight.DEF_INJN"
"DEF_INJF" > "HOLLight.hollight.DEF_INJF"
"DEF_INJA" > "HOLLight.hollight.DEF_INJA"
"DEF_INJ" > "HOLLight.hollight.DEF_INJ"
"DEF_INFINITE" > "HOLLightCompat.DEF_INFINITE"
"DEF_IND_SUC" > "HOLLight.hollight.DEF_IND_SUC"
"DEF_IND_0" > "HOLLight.hollight.DEF_IND_0"
"DEF_IN" > "Set.mem_def"
"DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE"
"DEF_I" > "Fun.id_apply"
"DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
"DEF_GSPEC" > "Set.Collect_def"
"DEF_GEQ" > "HOLLightCompat.DEF_GEQ"
"DEF_GABS" > "HOLLightCompat.DEF_GABS"
"DEF_FST" > "HOLLightCompat.DEF_FST"
"DEF_FNIL" > "HOLLight.hollight.DEF_FNIL"
"DEF_FINREC" > "HOLLight.hollight.DEF_FINREC"
"DEF_FINITE" > "HOLLightCompat.DEF_FINITE"
"DEF_FILTER" > "HOLLightList.DEF_FILTER"
"DEF_FCONS" > "HOLLight.hollight.DEF_FCONS"
"DEF_FACT" > "HOLLightCompat.DEF_FACT"
"DEF_F" > "HOL.False_def"
"DEF_EXP" > "HOLLightCompat.DEF_EXP"
"DEF_EX" > "HOLLightList.DEF_EX"
"DEF_EVEN" > "HOLLightCompat.DEF_EVEN"
"DEF_EMPTY" > "HOLLightCompat.DEF_EMPTY"
"DEF_EL" > "HOLLightList.DEF_EL"
"DEF_DIV" > "HOLLightCompat.DEF_DIV"
"DEF_DISJOINT" > "HOLLightCompat.DEF_DISJOINT"
"DEF_DIFF" > "HOLLightCompat.DEF_DIFF"
"DEF_DELETE" > "HOLLightCompat.DEF_DELETE"
"DEF_DECIMAL" > "HOLLight.hollight.DEF_DECIMAL"
"DEF_CURRY" > "Product_Type.curry_conv"
"DEF_CROSS" > "HOLLight.hollight.DEF_CROSS"
"DEF_COUNTABLE" > "HOLLight.hollight.DEF_COUNTABLE"
"DEF_CONSTR" > "HOLLight.hollight.DEF_CONSTR"
"DEF_COND" > "HOLLightCompat.COND_DEF"
"DEF_CHOICE" > "HOLLightCompat.DEF_CHOICE"
"DEF_CASEWISE" > "HOLLight.hollight.DEF_CASEWISE"
"DEF_CARD" > "HOLLight.hollight.DEF_CARD"
"DEF_BUTLAST" > "HOLLightList.DEF_BUTLAST"
"DEF_BOTTOM" > "HOLLight.hollight.DEF_BOTTOM"
"DEF_BIT1" > "HOLLightCompat.BIT1_DEF"
"DEF_BIT0" > "HOLLightCompat.BIT0_DEF"
"DEF_BIJ" > "HOLLight.hollight.DEF_BIJ"
"DEF_ASCII" > "HOLLight.hollight.DEF_ASCII"
"DEF_APPEND" > "HOLLightList.DEF_APPEND"
"DEF_ALL2" > "HOLLightList.DEF_ALL2"
"DEF_ALL" > "HOLLightList.DEF_ALL"
"DEF_-" > "HOLLightCompat.DEF_MINUS"
"DEF_+" > "HOLLightCompat.DEF_PLUS"
"DEF_$" > "HOLLight.hollight.DEF_$"
"DECOMPOSITION" > "HOLLight.hollight.DECOMPOSITION"
"DECIMAL_def" > "HOLLight.hollight.DECIMAL_def"
"CROSS_def" > "HOLLight.hollight.CROSS_def"
"CROSS_EQ_EMPTY" > "HOLLight.hollight.CROSS_EQ_EMPTY"
"COUNTABLE_def" > "HOLLight.hollight.COUNTABLE_def"
"CONS_HD_TL" > "List.hd_Cons_tl"
"CONS_11" > "List.list.inject"
"CONSTR_def" > "HOLLight.hollight.CONSTR_def"
"CONSTR_REC" > "HOLLight.hollight.CONSTR_REC"
"CONSTR_INJ" > "HOLLight.hollight.CONSTR_INJ"
"CONSTR_IND" > "HOLLight.hollight.CONSTR_IND"
"CONSTR_BOT" > "HOLLight.hollight.CONSTR_BOT"
"CONJ_SYM" > "Groebner_Basis.dnf_3"
"CONJ_ASSOC" > "HOL.conj_ac_3"
"CONJ_ACI" > "HOLLight.hollight.CONJ_ACI"
"COND_RATOR" > "HOLLight.hollight.COND_RATOR"
"COND_RAND" > "HOL.if_distrib"
"COND_ID" > "HOL.if_cancel"
"COND_EXPAND" > "HOLLight.hollight.COND_EXPAND"
"COND_EQ_CLAUSE" > "HOLLight.hollight.COND_EQ_CLAUSE"
"COND_ELIM_THM" > "HOL.if_splits_1"
"COND_CLAUSES" > "HOLLight.hollight.COND_CLAUSES"
"COND_ABS" > "HOLLight.hollight.COND_ABS"
"COMPONENT" > "Set.insertI1"
"CHOOSE_SUBSET_STRONG" > "HOLLight.hollight.CHOOSE_SUBSET_STRONG"
"CHOOSE_SUBSET" > "HOLLight.hollight.CHOOSE_SUBSET"
"CHOICE_DEF" > "HOLLight.hollight.CHOICE_DEF"
"CASEWISE_def" > "HOLLight.hollight.CASEWISE_def"
"CART_EQ_FULL" > "HOLLight.hollight.CART_EQ_FULL"
"CART_EQ" > "HOLLight.hollight.CART_EQ"
"CARD_def" > "HOLLight.hollight.CARD_def"
"CARD_UNION_OVERLAP_EQ" > "HOLLight.hollight.CARD_UNION_OVERLAP_EQ"
"CARD_UNION_OVERLAP" > "HOLLight.hollight.CARD_UNION_OVERLAP"
"CARD_UNION_LE" > "HOLLight.hollight.CARD_UNION_LE"
"CARD_UNION_GEN" > "HOLLight.hollight.CARD_UNION_GEN"
"CARD_UNION_EQ" > "HOLLight.hollight.CARD_UNION_EQ"
"CARD_UNIONS_LE" > "HOLLight.hollight.CARD_UNIONS_LE"
"CARD_UNIONS" > "HOLLight.hollight.CARD_UNIONS"
"CARD_UNION" > "HOLLight.hollight.CARD_UNION"
"CARD_SUBSET_LE" > "HOLLight.hollight.CARD_SUBSET_LE"
"CARD_SUBSET_IMAGE" > "HOLLight.hollight.CARD_SUBSET_IMAGE"
"CARD_SUBSET_EQ" > "HOLLight.hollight.CARD_SUBSET_EQ"
"CARD_SUBSET" > "HOLLight.hollight.CARD_SUBSET"
"CARD_PSUBSET" > "HOLLight.hollight.CARD_PSUBSET"
"CARD_PRODUCT" > "HOLLight.hollight.CARD_PRODUCT"
"CARD_POWERSET" > "HOLLight.hollight.CARD_POWERSET"
"CARD_NUMSEG_LT" > "HOLLight.hollight.CARD_NUMSEG_LT"
"CARD_NUMSEG_LEMMA" > "HOLLight.hollight.CARD_NUMSEG_LEMMA"
"CARD_NUMSEG_LE" > "HOLLight.hollight.CARD_NUMSEG_LE"
"CARD_NUMSEG_1" > "HOLLight.hollight.CARD_NUMSEG_1"
"CARD_NUMSEG" > "HOLLight.hollight.CARD_NUMSEG"
"CARD_LE_INJ" > "HOLLight.hollight.CARD_LE_INJ"
"CARD_IMAGE_LE" > "HOLLight.hollight.CARD_IMAGE_LE"
"CARD_IMAGE_INJ_EQ" > "HOLLight.hollight.CARD_IMAGE_INJ_EQ"
"CARD_IMAGE_INJ" > "HOLLight.hollight.CARD_IMAGE_INJ"
"CARD_FUNSPACE" > "HOLLight.hollight.CARD_FUNSPACE"
"CARD_FINITE_IMAGE" > "HOLLight.hollight.CARD_FINITE_IMAGE"
"CARD_EQ_SUM" > "HOLLight.hollight.CARD_EQ_SUM"
"CARD_EQ_NSUM" > "HOLLight.hollight.CARD_EQ_NSUM"
"CARD_EQ_BIJECTIONS" > "HOLLight.hollight.CARD_EQ_BIJECTIONS"
"CARD_EQ_BIJECTION" > "HOLLight.hollight.CARD_EQ_BIJECTION"
"CARD_EQ_0" > "HOLLight.hollight.CARD_EQ_0"
"CARD_DIFF" > "HOLLight.hollight.CARD_DIFF"
"CARD_DELETE" > "HOLLight.hollight.CARD_DELETE"
"CARD_CROSS" > "HOLLight.hollight.CARD_CROSS"
"CARD_CLAUSES" > "HOLLight.hollight.CARD_CLAUSES"
"BOUNDS_NOTZERO" > "HOLLight.hollight.BOUNDS_NOTZERO"
"BOUNDS_LINEAR_0" > "HOLLight.hollight.BOUNDS_LINEAR_0"
"BOUNDS_LINEAR" > "HOLLight.hollight.BOUNDS_LINEAR"
"BOUNDS_IGNORE" > "HOLLight.hollight.BOUNDS_IGNORE"
"BOUNDS_DIVIDED" > "HOLLight.hollight.BOUNDS_DIVIDED"
"BOTTOM_def" > "HOLLight.hollight.BOTTOM_def"
"BOOL_CASES_AX" > "HOL.True_or_False"
"BIT1_THM" > "HOLLight.hollight.BIT1_THM"
"BIT1" > "HOLLight.hollight.BIT1"
"BIT0_THM" > "Int.semiring_mult_2"
"BIT0" > "Int.semiring_mult_2"
"BIJ_def" > "HOLLight.hollight.BIJ_def"
"BIJECTIVE_ON_LEFT_RIGHT_INVERSE" > "HOLLight.hollight.BIJECTIVE_ON_LEFT_RIGHT_INVERSE"
"BIJECTIVE_LEFT_RIGHT_INVERSE" > "HOLLight.hollight.BIJECTIVE_LEFT_RIGHT_INVERSE"
"BIJECTIONS_HAS_SIZE_EQ" > "HOLLight.hollight.BIJECTIONS_HAS_SIZE_EQ"
"BIJECTIONS_HAS_SIZE" > "HOLLight.hollight.BIJECTIONS_HAS_SIZE"
"BIJECTIONS_CARD_EQ" > "HOLLight.hollight.BIJECTIONS_CARD_EQ"
"BETA_THM" > "HOL.eta_contract_eq"
"ASCII_def" > "HOLLight.hollight.ASCII_def"
"ARITH_ZERO" > "HOLLight.hollight.ARITH_ZERO"
"ARITH_SUC" > "HOLLight.hollight.ARITH_SUC"
"ARITH_SUB" > "HOLLight.hollight.ARITH_SUB"
"ARITH_PRE" > "HOLLight.hollight.ARITH_PRE"
"ARITH_ODD" > "HOLLight.hollight.ARITH_ODD"
"ARITH_MULT" > "HOLLight.hollight.ARITH_MULT"
"ARITH_LT" > "HOLLight.hollight.ARITH_LT"
"ARITH_LE" > "HOLLight.hollight.ARITH_LE"
"ARITH_EXP" > "HOLLight.hollight.ARITH_EXP"
"ARITH_EVEN" > "HOLLight.hollight.ARITH_EVEN"
"ARITH_EQ" > "HOLLight.hollight.ARITH_EQ"
"ARITH_ADD" > "HOLLight.hollight.ARITH_ADD"
"APPEND_NIL" > "List.append_Nil2"
"APPEND_EQ_NIL" > "List.append_is_Nil_conv"
"APPEND_BUTLAST_LAST" > "List.append_butlast_last_id"
"APPEND_ASSOC" > "List.append_assoc"
"AND_FORALL_THM" > "HOL.all_conj_distrib"
"AND_CLAUSES" > "HOLLight.hollight.AND_CLAUSES"
"AND_ALL2" > "HOLLightList.AND_ALL2"
"AND_ALL" > "HOLLightList.AND_ALL"
"ALL_T" > "HOLLightList.ALL_T"
"ALL_MP" > "HOLLightList.ALL_MP"
"ALL_MEM" > "HOLLightList.ALL_MEM"
"ALL_IMP" > "HOLLightList.ALL_IMP"
"ALL_EL" > "List.list_all_length"
"ALL_APPEND" > "List.list_all_append"
"ALL2_MAP2" > "HOLLightList.ALL2_MAP2"
"ALL2_MAP" > "HOLLightList.ALL2_MAP"
"ALL2_AND_RIGHT" > "HOLLightList.ALL2_AND_RIGHT"
"ALL2_ALL" > "HOLLightList.ALL2_ALL"
"ALL2" > "HOLLightList.ALL2"
"ADMISSIBLE_UNGUARDED_PATTERN" > "HOLLight.hollight.ADMISSIBLE_UNGUARDED_PATTERN"
"ADMISSIBLE_SUM" > "HOLLight.hollight.ADMISSIBLE_SUM"
"ADMISSIBLE_SEQPATTERN" > "HOLLight.hollight.ADMISSIBLE_SEQPATTERN"
"ADMISSIBLE_RAND" > "HOLLight.hollight.ADMISSIBLE_RAND"
"ADMISSIBLE_NSUM" > "HOLLight.hollight.ADMISSIBLE_NSUM"
"ADMISSIBLE_NEST" > "HOLLight.hollight.ADMISSIBLE_NEST"
"ADMISSIBLE_MATCH_SEQPATTERN" > "HOLLight.hollight.ADMISSIBLE_MATCH_SEQPATTERN"
"ADMISSIBLE_MATCH" > "HOLLight.hollight.ADMISSIBLE_MATCH"
"ADMISSIBLE_MAP" > "HOLLight.hollight.ADMISSIBLE_MAP"
"ADMISSIBLE_LAMBDA" > "HOLLight.hollight.ADMISSIBLE_LAMBDA"
"ADMISSIBLE_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.ADMISSIBLE_IMP_SUPERADMISSIBLE"
"ADMISSIBLE_GUARDED_PATTERN" > "HOLLight.hollight.ADMISSIBLE_GUARDED_PATTERN"
"ADMISSIBLE_CONST" > "HOLLight.hollight.ADMISSIBLE_CONST"
"ADMISSIBLE_COND" > "HOLLight.hollight.ADMISSIBLE_COND"
"ADMISSIBLE_COMB" > "HOLLight.hollight.ADMISSIBLE_COMB"
"ADMISSIBLE_BASE" > "HOLLight.hollight.ADMISSIBLE_BASE"
"ADD_SYM" > "Fields.linordered_field_class.sign_simps_43"
"ADD_SUC" > "Nat.add_Suc_right"
"ADD_SUBR2" > "Nat.diff_add_0"
"ADD_SUBR" > "HOLLight.hollight.ADD_SUBR"
"ADD_SUB2" > "Nat.diff_add_inverse"
"ADD_SUB" > "Nat.diff_add_inverse2"
"ADD_EQ_0" > "Nat.add_is_0"
"ADD_CLAUSES" > "HOLLight.hollight.ADD_CLAUSES"
"ADD_ASSOC" > "Fields.linordered_field_class.sign_simps_44"
"ADD_AC" > "HOLLight.hollight.ADD_AC"
"ADD_0" > "Divides.arithmetic_simps_39"
"ADD1" > "Nat_Numeral.Suc_eq_plus1"
"ABS_SIMP" > "HOL.refl"
"ABSORPTION" > "HOLLight.hollight.ABSORPTION"
">_c_def" > "HOLLight.hollight.>_c_def"
">=_c_def" > "HOLLight.hollight.>=_c_def"
"=_c_def" > "HOLLight.hollight.=_c_def"
"<_c_def" > "HOLLight.hollight.<_c_def"
"<=_c_def" > "HOLLight.hollight.<=_c_def"
"$_def" > "HOLLight.hollight.$_def"
ignore_thms
"WF_REC_CASES"
"TYDEF_sum"
"TYDEF_prod"
"TYDEF_option"
"TYDEF_num"
"TYDEF_list"
"TYDEF_1"
"SNDCART_PASTECART"
"SET_OF_LIST_OF_SET"
"REP_ABS_PAIR"
"RECURSION_CASEWISE_PAIRWISE"
"RECURSION_CASEWISE"
"PASTECART_FST_SND"
"PASTECART_EQ"
"MEM_LIST_OF_SET"
"MEM_ASSOC"
"LIST_OF_SET_PROPERTIES"
"LENGTH_LIST_OF_SET"
"HAS_SIZE_SET_OF_LIST"
"FSTCART_PASTECART"
"FORALL_PASTECART"
"FINITE_SET_OF_LIST"
"EX_MAP"
"EXISTS_PASTECART"
"EL_TL"
"DIMINDEX_HAS_SIZE_FINITE_SUM"
"DIMINDEX_FINITE_SUM"
"DEF_one"
"DEF_mk_pair"
"DEF_list_of_set"
"DEF__0"
"DEF_ZIP"
"DEF_TL"
"DEF_SUC"
"DEF_SOME"
"DEF_OUTR"
"DEF_OUTL"
"DEF_NONE"
"DEF_NIL"
"DEF_MAP2"
"DEF_ITLIST2"
"DEF_INR"
"DEF_INL"
"DEF_HD"
"DEF_CONS"
"DEF_ASSOC"
"DEF_,"
"CASEWISE_WORKS"
"CASEWISE_CASES"
"CASEWISE"
"CARD_SET_OF_LIST_LE"
"ALL_MAP"
end