src/HOL/Import/HOLLight/hollight.imp

Add icon for interface.

import

import_segment "hollight"

def_maps
  "two_2" > "two_2_def"
  "two_1" > "two_1_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"
  "three_3" > "three_3_def"
  "three_2" > "three_2_def"
  "three_1" > "three_1_def"
  "tendsto" > "tendsto_def"
  "tends_real_real" > "tends_real_real_def"
  "tends_num_real" > "tends_num_real_def"
  "tends" > "tends_def"
  "tdiv" > "tdiv_def"
  "tan" > "tan_def"
  "tailadmissible" > "tailadmissible_def"
  "support" > "support_def"
  "superadmissible" > "superadmissible_def"
  "sup" > "sup_def"
  "sums" > "sums_def"
  "summable" > "summable_def"
  "suminf" > "suminf_def"
  "sum" > "sum_def"
  "subseq" > "subseq_def"
  "sqrt" > "sqrt_def"
  "sndcart" > "sndcart_def"
  "sin" > "sin_def"
  "set_of_list" > "set_of_list_def"
  "rsum" > "rsum_def"
  "root" > "root_def"
  "real_sub" > "real_sub_def"
  "real_pow" > "real_pow_def"
  "real_of_num" > "real_of_num_def"
  "real_neg" > "real_neg_def"
  "real_mul" > "real_mul_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"
  "re_universe" > "re_universe_def"
  "re_union" > "re_union_def"
  "re_subset" > "re_subset_def"
  "re_null" > "re_null_def"
  "re_intersect" > "re_intersect_def"
  "re_compl" > "re_compl_def"
  "re_Union" > "re_Union_def"
  "psum" > "psum_def"
  "pi" > "pi_def"
  "pastecart" > "pastecart_def"
  "pairwise" > "pairwise_def"
  "nsum" > "nsum_def"
  "neutral" > "neutral_def"
  "neigh" > "neigh_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"
  "mtop" > "mtop_def"
  "mr1" > "mr1_def"
  "monoidal" > "monoidal_def"
  "mono" > "mono_def"
  "mod_real" > "mod_real_def"
  "mod_nat" > "mod_nat_def"
  "mod_int" > "mod_int_def"
  "minimal" > "minimal_def"
  "measure" > "measure_def"
  "ln" > "ln_def"
  "list_of_set" > "list_of_set_def"
  "limpt" > "limpt_def"
  "lim" > "lim_def"
  "lambda" > "lambda_def"
  "iterate" > "iterate_def"
  "istopology" > "istopology_def"
  "ismet" > "ismet_def"
  "is_nadd" > "is_nadd_def"
  "is_int" > "is_int_def"
  "int_sub" > "int_sub_def"
  "int_pow" > "int_pow_def"
  "int_of_num" > "int_of_num_def"
  "int_neg" > "int_neg_def"
  "int_mul" > "int_mul_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_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"
  "gauge" > "gauge_def"
  "fstcart" > "fstcart_def"
  "finite_index" > "finite_index_def"
  "fine" > "fine_def"
  "exp" > "exp_def"
  "eqeq" > "eqeq_def"
  "dsize" > "dsize_def"
  "dotdot" > "dotdot_def"
  "dorder" > "dorder_def"
  "division" > "division_def"
  "dist" > "dist_def"
  "dimindex" > "dimindex_def"
  "diffs" > "diffs_def"
  "diffl" > "diffl_def"
  "differentiable" > "differentiable_def"
  "defint" > "defint_def"
  "cos" > "cos_def"
  "convergent" > "convergent_def"
  "contl" > "contl_def"
  "closed" > "closed_def"
  "cauchy" > "cauchy_def"
  "bounded" > "bounded_def"
  "ball" > "ball_def"
  "atn" > "atn_def"
  "asn" > "asn_def"
  "admissible" > "admissible_def"
  "acs" > "acs_def"
  "_FALSITY_" > "_FALSITY__def"
  "_10314" > "_10314_def"
  "_10313" > "_10313_def"
  "_10312" > "_10312_def"
  "_10289" > "_10289_def"
  "_10288" > "_10288_def"
  "ZRECSPACE" > "ZRECSPACE_def"
  "ZIP" > "ZIP_def"
  "ZCONSTR" > "ZCONSTR_def"
  "ZBOT" > "ZBOT_def"
  "WF" > "WF_def"
  "UNIV" > "UNIV_def"
  "UNIONS" > "UNIONS_def"
  "UNION" > "UNION_def"
  "UNCURRY" > "UNCURRY_def"
  "TL" > "TL_def"
  "SURJ" > "SURJ_def"
  "SUBSET" > "SUBSET_def"
  "SOME" > "SOME_def"
  "SING" > "SING_def"
  "SETSPEC" > "SETSPEC_def"
  "REVERSE" > "REVERSE_def"
  "REST" > "REST_def"
  "REPLICATE" > "REPLICATE_def"
  "PSUBSET" > "PSUBSET_def"
  "PASSOC" > "PASSOC_def"
  "PAIRWISE" > "PAIRWISE_def"
  "OUTR" > "OUTR_def"
  "OUTL" > "OUTL_def"
  "ODD" > "ODD_def"
  "NUMSUM" > "NUMSUM_def"
  "NUMSND" > "NUMSND_def"
  "NUMRIGHT" > "NUMRIGHT_def"
  "NUMPAIR" > "NUMPAIR_def"
  "NUMLEFT" > "NUMLEFT_def"
  "NUMFST" > "NUMFST_def"
  "NULL" > "NULL_def"
  "NONE" > "NONE_def"
  "NIL" > "NIL_def"
  "MOD" > "MOD_def"
  "MEM" > "MEM_def"
  "MAP2" > "MAP2_def"
  "MAP" > "MAP_def"
  "LET_END" > "LET_END_def"
  "LENGTH" > "LENGTH_def"
  "LAST" > "LAST_def"
  "ITSET" > "ITSET_def"
  "ITLIST2" > "ITLIST2_def"
  "ITLIST" > "ITLIST_def"
  "ISO" > "ISO_def"
  "INTERS" > "INTERS_def"
  "INTER" > "INTER_def"
  "INSERT" > "INSERT_def"
  "INR" > "INR_def"
  "INL" > "INL_def"
  "INJP" > "INJP_def"
  "INJN" > "INJN_def"
  "INJF" > "INJF_def"
  "INJA" > "INJA_def"
  "INJ" > "INJ_def"
  "INFINITE" > "INFINITE_def"
  "IN" > "IN_def"
  "IMAGE" > "IMAGE_def"
  "HD" > "HD_def"
  "HAS_SIZE" > "HAS_SIZE_def"
  "GSPEC" > "GSPEC_def"
  "GEQ" > "GEQ_def"
  "GABS" > "GABS_def"
  "FNIL" > "FNIL_def"
  "FINREC" > "FINREC_def"
  "FINITE" > "FINITE_def"
  "FILTER" > "FILTER_def"
  "FCONS" > "FCONS_def"
  "FACT" > "FACT_def"
  "EXP" > "EXP_def"
  "EX" > "EX_def"
  "EVEN" > "EVEN_def"
  "EMPTY" > "EMPTY_def"
  "EL" > "EL_def"
  "DIV" > "DIV_def"
  "DISJOINT" > "DISJOINT_def"
  "DIFF" > "DIFF_def"
  "DELETE" > "DELETE_def"
  "DECIMAL" > "DECIMAL_def"
  "CURRY" > "CURRY_def"
  "COUNTABLE" > "COUNTABLE_def"
  "CONSTR" > "CONSTR_def"
  "CONS" > "CONS_def"
  "COND" > "COND_def"
  "CHOICE" > "CHOICE_def"
  "CASEWISE" > "CASEWISE_def"
  "CARD_LT" > "CARD_LT_def"
  "CARD_LE" > "CARD_LE_def"
  "CARD_GT" > "CARD_GT_def"
  "CARD_GE" > "CARD_GE_def"
  "CARD_EQ" > "CARD_EQ_def"
  "CARD" > "CARD_def"
  "BOTTOM" > "BOTTOM_def"
  "BIJ" > "BIJ_def"
  "ASSOC" > "ASSOC_def"
  "APPEND" > "APPEND_def"
  "ALL_list" > "ALL_list_def"
  "ALL2" > "ALL2_def"
  ">=" > ">=_def"
  ">" > ">_def"
  "<=" > "<=_def"
  "<" > "<_def"
  "$" > "$_def"

type_maps
  "topology" > "HOLLight.hollight.topology"
  "sum" > "HOLLight.hollight.sum"
  "recspace" > "HOLLight.hollight.recspace"
  "real" > "HOLLight.hollight.real"
  "prod" > "*"
  "option" > "HOLLight.hollight.option"
  "num" > "nat"
  "nadd" > "HOLLight.hollight.nadd"
  "metric" > "HOLLight.hollight.metric"
  "list" > "HOLLight.hollight.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"
  "cart" > "HOLLight.hollight.cart"
  "bool" > "bool"
  "N_3" > "HOLLight.hollight.N_3"
  "N_2" > "HOLLight.hollight.N_2"
  "N_1" > "Product_Type.unit"

const_maps
  "~" > "Not"
  "two_2" > "HOLLight.hollight.two_2"
  "two_1" > "HOLLight.hollight.two_1"
  "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"
  "three_3" > "HOLLight.hollight.three_3"
  "three_2" > "HOLLight.hollight.three_2"
  "three_1" > "HOLLight.hollight.three_1"
  "tendsto" > "HOLLight.hollight.tendsto"
  "tends_real_real" > "HOLLight.hollight.tends_real_real"
  "tends_num_real" > "HOLLight.hollight.tends_num_real"
  "tends" > "HOLLight.hollight.tends"
  "tdiv" > "HOLLight.hollight.tdiv"
  "tan" > "HOLLight.hollight.tan"
  "tailadmissible" > "HOLLight.hollight.tailadmissible"
  "support" > "HOLLight.hollight.support"
  "superadmissible" > "HOLLight.hollight.superadmissible"
  "sup" > "HOLLight.hollight.sup"
  "sums" > "HOLLight.hollight.sums"
  "summable" > "HOLLight.hollight.summable"
  "suminf" > "HOLLight.hollight.suminf"
  "sum" > "HOLLight.hollight.sum"
  "subseq" > "HOLLight.hollight.subseq"
  "sqrt" > "HOLLight.hollight.sqrt"
  "sndcart" > "HOLLight.hollight.sndcart"
  "sin" > "HOLLight.hollight.sin"
  "set_of_list" > "HOLLight.hollight.set_of_list"
  "rsum" > "HOLLight.hollight.rsum"
  "root" > "HOLLight.hollight.root"
  "real_sub" > "HOLLight.hollight.real_sub"
  "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_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"
  "re_universe" > "HOLLight.hollight.re_universe"
  "re_union" > "HOLLight.hollight.re_union"
  "re_subset" > "HOLLight.hollight.re_subset"
  "re_null" > "HOLLight.hollight.re_null"
  "re_intersect" > "HOLLight.hollight.re_intersect"
  "re_compl" > "HOLLight.hollight.re_compl"
  "re_Union" > "HOLLight.hollight.re_Union"
  "psum" > "HOLLight.hollight.psum"
  "pi" > "HOLLight.hollight.pi"
  "pastecart" > "HOLLight.hollight.pastecart"
  "pairwise" > "HOLLight.hollight.pairwise"
  "one" > "Product_Type.Unity"
  "o" > "Fun.comp"
  "nsum" > "HOLLight.hollight.nsum"
  "neutral" > "HOLLight.hollight.neutral"
  "neigh" > "HOLLight.hollight.neigh"
  "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"
  "mtop" > "HOLLight.hollight.mtop"
  "mr1" > "HOLLight.hollight.mr1"
  "monoidal" > "HOLLight.hollight.monoidal"
  "mono" > "HOLLight.hollight.mono"
  "mod_real" > "HOLLight.hollight.mod_real"
  "mod_nat" > "HOLLight.hollight.mod_nat"
  "mod_int" > "HOLLight.hollight.mod_int"
  "mk_pair" > "Product_Type.Pair_Rep"
  "minimal" > "HOLLight.hollight.minimal"
  "measure" > "HOLLight.hollight.measure"
  "ln" > "HOLLight.hollight.ln"
  "list_of_set" > "HOLLight.hollight.list_of_set"
  "limpt" > "HOLLight.hollight.limpt"
  "lim" > "HOLLight.hollight.lim"
  "lambda" > "HOLLight.hollight.lambda"
  "iterate" > "HOLLight.hollight.iterate"
  "istopology" > "HOLLight.hollight.istopology"
  "ismet" > "HOLLight.hollight.ismet"
  "is_nadd" > "HOLLight.hollight.is_nadd"
  "is_int" > "HOLLight.hollight.is_int"
  "int_sub" > "HOLLight.hollight.int_sub"
  "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_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_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"
  "gauge" > "HOLLight.hollight.gauge"
  "fstcart" > "HOLLight.hollight.fstcart"
  "finite_index" > "HOLLight.hollight.finite_index"
  "fine" > "HOLLight.hollight.fine"
  "exp" > "HOLLight.hollight.exp"
  "eqeq" > "HOLLight.hollight.eqeq"
  "dsize" > "HOLLight.hollight.dsize"
  "dotdot" > "HOLLight.hollight.dotdot"
  "dorder" > "HOLLight.hollight.dorder"
  "division" > "HOLLight.hollight.division"
  "dist" > "HOLLight.hollight.dist"
  "dimindex" > "HOLLight.hollight.dimindex"
  "diffs" > "HOLLight.hollight.diffs"
  "diffl" > "HOLLight.hollight.diffl"
  "differentiable" > "HOLLight.hollight.differentiable"
  "defint" > "HOLLight.hollight.defint"
  "cos" > "HOLLight.hollight.cos"
  "convergent" > "HOLLight.hollight.convergent"
  "contl" > "HOLLight.hollight.contl"
  "closed" > "HOLLight.hollight.closed"
  "cauchy" > "HOLLight.hollight.cauchy"
  "bounded" > "HOLLight.hollight.bounded"
  "ball" > "HOLLight.hollight.ball"
  "atn" > "HOLLight.hollight.atn"
  "asn" > "HOLLight.hollight.asn"
  "admissible" > "HOLLight.hollight.admissible"
  "acs" > "HOLLight.hollight.acs"
  "_FALSITY_" > "HOLLight.hollight._FALSITY_"
  "_10314" > "HOLLight.hollight._10314"
  "_10313" > "HOLLight.hollight._10313"
  "_10312" > "HOLLight.hollight._10312"
  "_10289" > "HOLLight.hollight._10289"
  "_10288" > "HOLLight.hollight._10288"
  "_0" > "0" :: "nat"
  "\\/" > "op |"
  "ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
  "ZIP" > "HOLLight.hollight.ZIP"
  "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
  "ZBOT" > "HOLLight.hollight.ZBOT"
  "WF" > "HOLLight.hollight.WF"
  "UNIV" > "HOLLight.hollight.UNIV"
  "UNIONS" > "HOLLight.hollight.UNIONS"
  "UNION" > "HOLLight.hollight.UNION"
  "UNCURRY" > "HOLLight.hollight.UNCURRY"
  "TL" > "HOLLight.hollight.TL"
  "T" > "True"
  "SURJ" > "HOLLight.hollight.SURJ"
  "SUC" > "Suc"
  "SUBSET" > "HOLLight.hollight.SUBSET"
  "SOME" > "HOLLight.hollight.SOME"
  "SND" > "snd"
  "SING" > "HOLLight.hollight.SING"
  "SETSPEC" > "HOLLight.hollight.SETSPEC"
  "REVERSE" > "HOLLight.hollight.REVERSE"
  "REST" > "HOLLight.hollight.REST"
  "REP_prod" > "Rep_Prod"
  "REPLICATE" > "HOLLight.hollight.REPLICATE"
  "PSUBSET" > "HOLLight.hollight.PSUBSET"
  "PRE" > "HOLLightCompat.Pred"
  "PASSOC" > "HOLLight.hollight.PASSOC"
  "PAIRWISE" > "HOLLight.hollight.PAIRWISE"
  "OUTR" > "HOLLight.hollight.OUTR"
  "OUTL" > "HOLLight.hollight.OUTL"
  "ONTO" > "Fun.surj"
  "ONE_ONE" > "HOL4Setup.ONE_ONE"
  "ODD" > "HOLLight.hollight.ODD"
  "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" > "HOL4Compat.NUMERAL"
  "NULL" > "HOLLight.hollight.NULL"
  "NONE" > "HOLLight.hollight.NONE"
  "NIL" > "HOLLight.hollight.NIL"
  "MOD" > "HOLLight.hollight.MOD"
  "MEM" > "HOLLight.hollight.MEM"
  "MAP2" > "HOLLight.hollight.MAP2"
  "MAP" > "HOLLight.hollight.MAP"
  "LET_END" > "HOLLight.hollight.LET_END"
  "LET" > "HOL4Compat.LET"
  "LENGTH" > "HOLLight.hollight.LENGTH"
  "LAST" > "HOLLight.hollight.LAST"
  "ITSET" > "HOLLight.hollight.ITSET"
  "ITLIST2" > "HOLLight.hollight.ITLIST2"
  "ITLIST" > "HOLLight.hollight.ITLIST"
  "ISO" > "HOLLight.hollight.ISO"
  "INTERS" > "HOLLight.hollight.INTERS"
  "INTER" > "HOLLight.hollight.INTER"
  "INSERT" > "HOLLight.hollight.INSERT"
  "INR" > "HOLLight.hollight.INR"
  "INL" > "HOLLight.hollight.INL"
  "INJP" > "HOLLight.hollight.INJP"
  "INJN" > "HOLLight.hollight.INJN"
  "INJF" > "HOLLight.hollight.INJF"
  "INJA" > "HOLLight.hollight.INJA"
  "INJ" > "HOLLight.hollight.INJ"
  "INFINITE" > "HOLLight.hollight.INFINITE"
  "IN" > "HOLLight.hollight.IN"
  "IMAGE" > "HOLLight.hollight.IMAGE"
  "I" > "Fun.id"
  "HD" > "HOLLight.hollight.HD"
  "HAS_SIZE" > "HOLLight.hollight.HAS_SIZE"
  "GSPEC" > "HOLLight.hollight.GSPEC"
  "GEQ" > "HOLLight.hollight.GEQ"
  "GABS" > "HOLLight.hollight.GABS"
  "FST" > "fst"
  "FNIL" > "HOLLight.hollight.FNIL"
  "FINREC" > "HOLLight.hollight.FINREC"
  "FINITE" > "HOLLight.hollight.FINITE"
  "FILTER" > "HOLLight.hollight.FILTER"
  "FCONS" > "HOLLight.hollight.FCONS"
  "FACT" > "HOLLight.hollight.FACT"
  "F" > "False"
  "EXP" > "HOLLight.hollight.EXP"
  "EX" > "HOLLight.hollight.EX"
  "EVEN" > "HOLLight.hollight.EVEN"
  "EMPTY" > "HOLLight.hollight.EMPTY"
  "EL" > "HOLLight.hollight.EL"
  "DIV" > "HOLLight.hollight.DIV"
  "DISJOINT" > "HOLLight.hollight.DISJOINT"
  "DIFF" > "HOLLight.hollight.DIFF"
  "DELETE" > "HOLLight.hollight.DELETE"
  "DECIMAL" > "HOLLight.hollight.DECIMAL"
  "CURRY" > "HOLLight.hollight.CURRY"
  "COUNTABLE" > "HOLLight.hollight.COUNTABLE"
  "CONSTR" > "HOLLight.hollight.CONSTR"
  "CONS" > "HOLLight.hollight.CONS"
  "COND" > "HOLLight.hollight.COND"
  "CHOICE" > "HOLLight.hollight.CHOICE"
  "CASEWISE" > "HOLLight.hollight.CASEWISE"
  "CARD_LT" > "HOLLight.hollight.CARD_LT"
  "CARD_LE" > "HOLLight.hollight.CARD_LE"
  "CARD_GT" > "HOLLight.hollight.CARD_GT"
  "CARD_GE" > "HOLLight.hollight.CARD_GE"
  "CARD_EQ" > "HOLLight.hollight.CARD_EQ"
  "CARD" > "HOLLight.hollight.CARD"
  "BOTTOM" > "HOLLight.hollight.BOTTOM"
  "BIT1" > "HOL4Compat.NUMERAL_BIT1"
  "BIT0" > "HOLLightCompat.NUMERAL_BIT0"
  "BIJ" > "HOLLight.hollight.BIJ"
  "ASSOC" > "HOLLight.hollight.ASSOC"
  "APPEND" > "HOLLight.hollight.APPEND"
  "ALL_list" > "HOLLight.hollight.ALL_list"
  "ALL2" > "HOLLight.hollight.ALL2"
  "ABS_prod" > "Abs_Prod"
  "@" > "Hilbert_Choice.Eps"
  "?!" > "Ex1"
  "?" > "Ex"
  ">=" > "HOLLight.hollight.>="
  ">" > "HOLLight.hollight.>"
  "==>" > "op -->"
  "=" > "op ="
  "<=" > "HOLLight.hollight.<="
  "<" > "HOLLight.hollight.<"
  "/\\" > "op &"
  "-" > "op -" :: "nat => nat => nat"
  "," > "Pair"
  "+" > "op +" :: "nat => nat => nat"
  "*" > "op *" :: "nat => nat => nat"
  "$" > "HOLLight.hollight.$"
  "!" > "All"

const_renames
  "ALL" > "ALL_list"
  "==" > "eqeq"
  ".." > "dotdot"

thm_maps
  "two_2_def" > "HOLLight.hollight.two_2_def"
  "two_1_def" > "HOLLight.hollight.two_1_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"
  "three_3_def" > "HOLLight.hollight.three_3_def"
  "three_2_def" > "HOLLight.hollight.three_2_def"
  "three_1_def" > "HOLLight.hollight.three_1_def"
  "th_cond" > "HOLLight.hollight.th_cond"
  "th" > "HOLLight.hollight.th"
  "tendsto_def" > "HOLLight.hollight.tendsto_def"
  "tends_real_real_def" > "HOLLight.hollight.tends_real_real_def"
  "tends_num_real_def" > "HOLLight.hollight.tends_num_real_def"
  "tends_def" > "HOLLight.hollight.tends_def"
  "tdiv_def" > "HOLLight.hollight.tdiv_def"
  "tan_def" > "HOLLight.hollight.tan_def"
  "tailadmissible_def" > "HOLLight.hollight.tailadmissible_def"
  "support_def" > "HOLLight.hollight.support_def"
  "superadmissible_def" > "HOLLight.hollight.superadmissible_def"
  "sup_def" > "HOLLight.hollight.sup_def"
  "sup" > "HOLLight.hollight.sup"
  "sums_def" > "HOLLight.hollight.sums_def"
  "summable_def" > "HOLLight.hollight.summable_def"
  "suminf_def" > "HOLLight.hollight.suminf_def"
  "sum_def" > "HOLLight.hollight.sum_def"
  "sum_EXISTS" > "HOLLight.hollight.sum_EXISTS"
  "sum" > "HOLLight.hollight.sum"
  "subseq_def" > "HOLLight.hollight.subseq_def"
  "sth" > "HOLLight.hollight.sth"
  "sqrt_def" > "HOLLight.hollight.sqrt_def"
  "sqrt" > "HOLLight.hollight.sqrt"
  "sndcart_def" > "HOLLight.hollight.sndcart_def"
  "sin_def" > "HOLLight.hollight.sin_def"
  "set_of_list_def" > "HOLLight.hollight.set_of_list_def"
  "rsum_def" > "HOLLight.hollight.rsum_def"
  "root_def" > "HOLLight.hollight.root_def"
  "right_th" > "HOLLight.hollight.right_th"
  "real_sub_def" > "HOLLight.hollight.real_sub_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_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_le" > "HOLLight.hollight.real_le"
  "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"
  "re_universe_def" > "HOLLight.hollight.re_universe_def"
  "re_union_def" > "HOLLight.hollight.re_union_def"
  "re_subset_def" > "HOLLight.hollight.re_subset_def"
  "re_null_def" > "HOLLight.hollight.re_null_def"
  "re_intersect_def" > "HOLLight.hollight.re_intersect_def"
  "re_compl_def" > "HOLLight.hollight.re_compl_def"
  "re_Union_def" > "HOLLight.hollight.re_Union_def"
  "psum_def" > "HOLLight.hollight.psum_def"
  "pi_def" > "HOLLight.hollight.pi_def"
  "pastecart_def" > "HOLLight.hollight.pastecart_def"
  "pairwise_def" > "HOLLight.hollight.pairwise_def"
  "pair_RECURSION" > "HOLLight.hollight.pair_RECURSION"
  "pair_INDUCT" > "Datatype.prod.induct"
  "one_axiom" > "HOLLight.hollight.one_axiom"
  "one_RECURSION" > "HOLLight.hollight.one_RECURSION"
  "one_INDUCT" > "Datatype.unit.induct"
  "one_Axiom" > "HOLLight.hollight.one_Axiom"
  "one" > "HOL4Compat.one"
  "o_THM" > "Fun.o_apply"
  "o_ASSOC" > "HOLLight.hollight.o_ASSOC"
  "num_WOP" > "HOLLight.hollight.num_WOP"
  "num_WF" > "HOLLight.hollight.num_WF"
  "num_RECURSION_STD" > "HOLLight.hollight.num_RECURSION_STD"
  "num_MAX" > "HOLLight.hollight.num_MAX"
  "num_INFINITE" > "HOLLight.hollight.num_INFINITE"
  "num_INDUCTION" > "List.lexn.induct"
  "num_FINITE_AVOID" > "HOLLight.hollight.num_FINITE_AVOID"
  "num_FINITE" > "HOLLight.hollight.num_FINITE"
  "num_CASES" > "Nat.nat.nchotomy"
  "num_Axiom" > "HOLLight.hollight.num_Axiom"
  "nsum_def" > "HOLLight.hollight.nsum_def"
  "neutral_def" > "HOLLight.hollight.neutral_def"
  "neigh_def" > "HOLLight.hollight.neigh_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"
  "mtop_istopology" > "HOLLight.hollight.mtop_istopology"
  "mtop_def" > "HOLLight.hollight.mtop_def"
  "mr1_def" > "HOLLight.hollight.mr1_def"
  "monoidal_def" > "HOLLight.hollight.monoidal_def"
  "mono_def" > "HOLLight.hollight.mono_def"
  "mod_real_def" > "HOLLight.hollight.mod_real_def"
  "mod_nat_def" > "HOLLight.hollight.mod_nat_def"
  "mod_int_def" > "HOLLight.hollight.mod_int_def"
  "minimal_def" > "HOLLight.hollight.minimal_def"
  "measure_def" > "HOLLight.hollight.measure_def"
  "ln_def" > "HOLLight.hollight.ln_def"
  "list_of_set_def" > "HOLLight.hollight.list_of_set_def"
  "list_INDUCT" > "HOLLight.hollight.list_INDUCT"
  "list_CASES" > "HOLLight.hollight.list_CASES"
  "limpt_def" > "HOLLight.hollight.limpt_def"
  "lim_def" > "HOLLight.hollight.lim_def"
  "lambda_def" > "HOLLight.hollight.lambda_def"
  "iterate_def" > "HOLLight.hollight.iterate_def"
  "istopology_def" > "HOLLight.hollight.istopology_def"
  "ismet_def" > "HOLLight.hollight.ismet_def"
  "is_nadd_def" > "HOLLight.hollight.is_nadd_def"
  "is_nadd_0" > "HOLLight.hollight.is_nadd_0"
  "is_int_def" > "HOLLight.hollight.is_int_def"
  "int_sub_th" > "HOLLight.hollight.int_sub_th"
  "int_sub_def" > "HOLLight.hollight.int_sub_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_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_eq" > "HOLLight.hollight.int.dest_int_inject"
  "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"
  "gauge_def" > "HOLLight.hollight.gauge_def"
  "fstcart_def" > "HOLLight.hollight.fstcart_def"
  "finite_index_def" > "HOLLight.hollight.finite_index_def"
  "fine_def" > "HOLLight.hollight.fine_def"
  "exp_def" > "HOLLight.hollight.exp_def"
  "eqeq_def" > "HOLLight.hollight.eqeq_def"
  "dsize_def" > "HOLLight.hollight.dsize_def"
  "dotdot_def" > "HOLLight.hollight.dotdot_def"
  "dorder_def" > "HOLLight.hollight.dorder_def"
  "division_def" > "HOLLight.hollight.division_def"
  "dist_def" > "HOLLight.hollight.dist_def"
  "dimindex_def" > "HOLLight.hollight.dimindex_def"
  "diffs_def" > "HOLLight.hollight.diffs_def"
  "diffl_def" > "HOLLight.hollight.diffl_def"
  "differentiable_def" > "HOLLight.hollight.differentiable_def"
  "dest_int_rep" > "HOLLight.hollight.dest_int_rep"
  "defint_def" > "HOLLight.hollight.defint_def"
  "cth" > "HOLLight.hollight.cth"
  "cos_def" > "HOLLight.hollight.cos_def"
  "convergent_def" > "HOLLight.hollight.convergent_def"
  "contl_def" > "HOLLight.hollight.contl_def"
  "closed_def" > "HOLLight.hollight.closed_def"
  "cauchy_def" > "HOLLight.hollight.cauchy_def"
  "bounded_def" > "HOLLight.hollight.bounded_def"
  "ball_def" > "HOLLight.hollight.ball_def"
  "ax__3" > "HOL4Setup.INFINITY_AX"
  "ax__2" > "Hilbert_Choice.tfl_some"
  "ax__1" > "Presburger.fm_modd_pinf"
  "atn_def" > "HOLLight.hollight.atn_def"
  "asn_def" > "HOLLight.hollight.asn_def"
  "admissible_def" > "HOLLight.hollight.admissible_def"
  "acs_def" > "HOLLight.hollight.acs_def"
  "_FALSITY__def" > "HOLLight.hollight._FALSITY__def"
  "_10314_def" > "HOLLight.hollight._10314_def"
  "_10313_def" > "HOLLight.hollight._10313_def"
  "_10312_def" > "HOLLight.hollight._10312_def"
  "_10289_def" > "HOLLight.hollight._10289_def"
  "_10288_def" > "HOLLight.hollight._10288_def"
  "ZRECSPACE_def" > "HOLLight.hollight.ZRECSPACE_def"
  "ZIP_def" > "HOLLight.hollight.ZIP_def"
  "ZIP" > "HOLLight.hollight.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_def" > "HOLLight.hollight.WF_def"
  "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_CASES" > "HOLLight.hollight.WF_REC_CASES"
  "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_IND" > "HOLLight.hollight.WF_IND"
  "WF_FALSE" > "HOLLight.hollight.WF_FALSE"
  "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_def" > "HOLLight.hollight.UNIV_def"
  "UNIV_SUBSET" > "HOLLight.hollight.UNIV_SUBSET"
  "UNIV_NOT_EMPTY" > "HOLLight.hollight.UNIV_NOT_EMPTY"
  "UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
  "UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
  "UNION_def" > "HOLLight.hollight.UNION_def"
  "UNION_UNIV" > "HOLLight.hollight.UNION_UNIV"
  "UNION_SUBSET" > "HOLLight.hollight.UNION_SUBSET"
  "UNION_OVER_INTER" > "HOLLight.hollight.UNION_OVER_INTER"
  "UNION_IDEMPOT" > "HOLLight.hollight.UNION_IDEMPOT"
  "UNION_EMPTY" > "HOLLight.hollight.UNION_EMPTY"
  "UNION_COMM" > "HOLLight.hollight.UNION_COMM"
  "UNION_ASSOC" > "HOLLight.hollight.UNION_ASSOC"
  "UNION_ACI" > "HOLLight.hollight.UNION_ACI"
  "UNIONS_def" > "HOLLight.hollight.UNIONS_def"
  "UNIONS_INSERT" > "HOLLight.hollight.UNIONS_INSERT"
  "UNIONS_2" > "HOLLight.hollight.UNIONS_2"
  "UNIONS_1" > "HOLLight.hollight.UNIONS_1"
  "UNIONS_0" > "HOLLight.hollight.UNIONS_0"
  "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
  "TYDEF_topology" > "HOLLight.hollight.TYDEF_topology"
  "TYDEF_sum" > "HOLLight.hollight.TYDEF_sum"
  "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
  "TYDEF_real" > "HOLLight.hollight.TYDEF_real"
  "TYDEF_option" > "HOLLight.hollight.TYDEF_option"
  "TYDEF_nadd" > "HOLLight.hollight.TYDEF_nadd"
  "TYDEF_metric" > "HOLLight.hollight.TYDEF_metric"
  "TYDEF_list" > "HOLLight.hollight.TYDEF_list"
  "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_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"
  "TOPOLOGY_UNION" > "HOLLight.hollight.TOPOLOGY_UNION"
  "TOPOLOGY" > "HOLLight.hollight.TOPOLOGY"
  "TL_def" > "HOLLight.hollight.TL_def"
  "TERMDIFF_STRONG" > "HOLLight.hollight.TERMDIFF_STRONG"
  "TERMDIFF_LEMMA5" > "HOLLight.hollight.TERMDIFF_LEMMA5"
  "TERMDIFF_LEMMA4" > "HOLLight.hollight.TERMDIFF_LEMMA4"
  "TERMDIFF_LEMMA3" > "HOLLight.hollight.TERMDIFF_LEMMA3"
  "TERMDIFF_LEMMA2" > "HOLLight.hollight.TERMDIFF_LEMMA2"
  "TERMDIFF_LEMMA1" > "HOLLight.hollight.TERMDIFF_LEMMA1"
  "TERMDIFF_CONVERGES" > "HOLLight.hollight.TERMDIFF_CONVERGES"
  "TERMDIFF" > "HOLLight.hollight.TERMDIFF"
  "TAN_TOTAL_POS" > "HOLLight.hollight.TAN_TOTAL_POS"
  "TAN_TOTAL_LEMMA" > "HOLLight.hollight.TAN_TOTAL_LEMMA"
  "TAN_TOTAL" > "HOLLight.hollight.TAN_TOTAL"
  "TAN_SEC" > "HOLLight.hollight.TAN_SEC"
  "TAN_POS_PI2" > "HOLLight.hollight.TAN_POS_PI2"
  "TAN_PI4" > "HOLLight.hollight.TAN_PI4"
  "TAN_PI" > "HOLLight.hollight.TAN_PI"
  "TAN_PERIODIC_PI" > "HOLLight.hollight.TAN_PERIODIC_PI"
  "TAN_PERIODIC_NPI" > "HOLLight.hollight.TAN_PERIODIC_NPI"
  "TAN_PERIODIC" > "HOLLight.hollight.TAN_PERIODIC"
  "TAN_NPI" > "HOLLight.hollight.TAN_NPI"
  "TAN_NEG" > "HOLLight.hollight.TAN_NEG"
  "TAN_DOUBLE" > "HOLLight.hollight.TAN_DOUBLE"
  "TAN_COT" > "HOLLight.hollight.TAN_COT"
  "TAN_BOUND_PI2" > "HOLLight.hollight.TAN_BOUND_PI2"
  "TAN_ATN" > "HOLLight.hollight.TAN_ATN"
  "TAN_ADD" > "HOLLight.hollight.TAN_ADD"
  "TAN_ABS_GE_X" > "HOLLight.hollight.TAN_ABS_GE_X"
  "TAN_0" > "HOLLight.hollight.TAN_0"
  "TAIL_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.TAIL_IMP_SUPERADMISSIBLE"
  "SWAP_FORALL_THM" > "HOLLight.hollight.SWAP_FORALL_THM"
  "SWAP_EXISTS_THM" > "HOLLight.hollight.SWAP_EXISTS_THM"
  "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_IFF_INJECTIVE_GEN" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE_GEN"
  "SURJECTIVE_IFF_INJECTIVE" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE"
  "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_T" > "HOLLight.hollight.SUPERADMISSIBLE_T"
  "SUPERADMISSIBLE_COND" > "HOLLight.hollight.SUPERADMISSIBLE_COND"
  "SUM_ZERO" > "HOLLight.hollight.SUM_ZERO"
  "SUM_UNIQ" > "HOLLight.hollight.SUM_UNIQ"
  "SUM_UNION_RZERO" > "HOLLight.hollight.SUM_UNION_RZERO"
  "SUM_UNION_LZERO" > "HOLLight.hollight.SUM_UNION_LZERO"
  "SUM_UNION_EQ" > "HOLLight.hollight.SUM_UNION_EQ"
  "SUM_UNION" > "HOLLight.hollight.SUM_UNION"
  "SUM_TWO" > "HOLLight.hollight.SUM_TWO"
  "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_SUMMABLE" > "HOLLight.hollight.SUM_SUMMABLE"
  "SUM_SUB_NUMSEG" > "HOLLight.hollight.SUM_SUB_NUMSEG"
  "SUM_SUBST" > "HOLLight.hollight.SUM_SUBST"
  "SUM_SUBSET_SIMPLE" > "HOLLight.hollight.SUM_SUBSET_SIMPLE"
  "SUM_SUBSET" > "HOLLight.hollight.SUM_SUBSET"
  "SUM_SUB" > "HOLLight.hollight.SUM_SUB"
  "SUM_SPLIT" > "HOLLight.hollight.SUM_SPLIT"
  "SUM_SING_NUMSEG" > "HOLLight.hollight.SUM_SING_NUMSEG"
  "SUM_SING" > "HOLLight.hollight.SUM_SING"
  "SUM_RESTRICT_SET" > "HOLLight.hollight.SUM_RESTRICT_SET"
  "SUM_RESTRICT" > "HOLLight.hollight.SUM_RESTRICT"
  "SUM_REINDEX" > "HOLLight.hollight.SUM_REINDEX"
  "SUM_POS_LE_NUMSEG" > "HOLLight.hollight.SUM_POS_LE_NUMSEG"
  "SUM_POS_LE" > "HOLLight.hollight.SUM_POS_LE"
  "SUM_POS_GEN" > "HOLLight.hollight.SUM_POS_GEN"
  "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_POS" > "HOLLight.hollight.SUM_POS"
  "SUM_OFFSET_0" > "HOLLight.hollight.SUM_OFFSET_0"
  "SUM_OFFSET" > "HOLLight.hollight.SUM_OFFSET"
  "SUM_NSUB" > "HOLLight.hollight.SUM_NSUB"
  "SUM_NEG_NUMSEG" > "HOLLight.hollight.SUM_NEG_NUMSEG"
  "SUM_NEG" > "HOLLight.hollight.SUM_NEG"
  "SUM_MULTICOUNT_GEN" > "HOLLight.hollight.SUM_MULTICOUNT_GEN"
  "SUM_MULTICOUNT" > "HOLLight.hollight.SUM_MULTICOUNT"
  "SUM_MORETERMS_EQ" > "HOLLight.hollight.SUM_MORETERMS_EQ"
  "SUM_LT_ALL" > "HOLLight.hollight.SUM_LT_ALL"
  "SUM_LT" > "HOLLight.hollight.SUM_LT"
  "SUM_LE_NUMSEG" > "HOLLight.hollight.SUM_LE_NUMSEG"
  "SUM_LE" > "HOLLight.hollight.SUM_LE"
  "SUM_IMAGE_GEN" > "HOLLight.hollight.SUM_IMAGE_GEN"
  "SUM_IMAGE" > "HOLLight.hollight.SUM_IMAGE"
  "SUM_HORNER" > "HOLLight.hollight.SUM_HORNER"
  "SUM_GROUP" > "HOLLight.hollight.SUM_GROUP"
  "SUM_EQ_SUPERSET" > "HOLLight.hollight.SUM_EQ_SUPERSET"
  "SUM_EQ_NUMSEG" > "HOLLight.hollight.SUM_EQ_NUMSEG"
  "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_DIFFERENCES_EQ" > "HOLLight.hollight.SUM_DIFFERENCES_EQ"
  "SUM_DIFF" > "HOLLight.hollight.SUM_DIFF"
  "SUM_DELTA" > "HOLLight.hollight.SUM_DELTA"
  "SUM_CONST_NUMSEG" > "HOLLight.hollight.SUM_CONST_NUMSEG"
  "SUM_CONST" > "HOLLight.hollight.SUM_CONST"
  "SUM_CMUL_NUMSEG" > "HOLLight.hollight.SUM_CMUL_NUMSEG"
  "SUM_CMUL" > "HOLLight.hollight.SUM_CMUL"
  "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_CANCEL" > "HOLLight.hollight.SUM_CANCEL"
  "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_ADD_SPLIT" > "HOLLight.hollight.SUM_ADD_SPLIT"
  "SUM_ADD_NUMSEG" > "HOLLight.hollight.SUM_ADD_NUMSEG"
  "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_2" > "HOLLight.hollight.SUM_2"
  "SUM_1" > "HOLLight.hollight.SUM_1"
  "SUM_0" > "HOLLight.hollight.SUM_0"
  "SUMMABLE_SUM" > "HOLLight.hollight.SUMMABLE_SUM"
  "SUC_SUB1" > "HOLLight.hollight.SUC_SUB1"
  "SUC_INJ" > "Nat.nat.simps_3"
  "SUB_SUC" > "Nat.diff_Suc_Suc"
  "SUB_SUB" > "HOLLight.hollight.SUB_SUB"
  "SUB_REFL" > "Nat.diff_self_eq_0"
  "SUB_PRESUC" > "HOLLight.hollight.SUB_PRESUC"
  "SUB_OLD" > "HOLLight.hollight.SUB_OLD"
  "SUB_EQ_0" > "HOLLight.hollight.SUB_EQ_0"
  "SUB_ELIM_THM" > "HOLLight.hollight.SUB_ELIM_THM"
  "SUB_ADD_RCANCEL" > "Nat.diff_cancel2"
  "SUB_ADD_LCANCEL" > "Nat.diff_cancel"
  "SUB_ADD" > "HOLLight.hollight.SUB_ADD"
  "SUB_0" > "HOLLight.hollight.SUB_0"
  "SUBSET_def" > "HOLLight.hollight.SUBSET_def"
  "SUBSET_UNIV" > "HOLLight.hollight.SUBSET_UNIV"
  "SUBSET_UNION_ABSORPTION" > "HOLLight.hollight.SUBSET_UNION_ABSORPTION"
  "SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
  "SUBSET_TRANS" > "HOLLight.hollight.SUBSET_TRANS"
  "SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
  "SUBSET_REFL" > "HOLLight.hollight.SUBSET_REFL"
  "SUBSET_PSUBSET_TRANS" > "HOLLight.hollight.SUBSET_PSUBSET_TRANS"
  "SUBSET_NUMSEG" > "HOLLight.hollight.SUBSET_NUMSEG"
  "SUBSET_INTER_ABSORPTION" > "HOLLight.hollight.SUBSET_INTER_ABSORPTION"
  "SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
  "SUBSET_INSERT" > "HOLLight.hollight.SUBSET_INSERT"
  "SUBSET_IMAGE" > "HOLLight.hollight.SUBSET_IMAGE"
  "SUBSET_EMPTY" > "HOLLight.hollight.SUBSET_EMPTY"
  "SUBSET_DIFF" > "HOLLight.hollight.SUBSET_DIFF"
  "SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
  "SUBSET_ANTISYM" > "HOLLight.hollight.SUBSET_ANTISYM"
  "SUBSETA_TRANS" > "HOLLight.hollight.SUBSETA_TRANS"
  "SUBSETA_REFL" > "HOLLight.hollight.SUBSETA_REFL"
  "SUBSETA_ANTISYM" > "HOLLight.hollight.SUBSETA_ANTISYM"
  "SUBSEQ_SUC" > "HOLLight.hollight.SUBSEQ_SUC"
  "STRADDLE_LEMMA" > "HOLLight.hollight.STRADDLE_LEMMA"
  "SQRT_POW_2" > "HOLLight.hollight.SQRT_POW_2"
  "SQRT_POW2" > "HOLLight.hollight.SQRT_POW2"
  "SQRT_POS_UNIQ" > "HOLLight.hollight.SQRT_POS_UNIQ"
  "SQRT_POS_LT" > "HOLLight.hollight.SQRT_POS_LT"
  "SQRT_POS_LE" > "HOLLight.hollight.SQRT_POS_LE"
  "SQRT_MUL" > "HOLLight.hollight.SQRT_MUL"
  "SQRT_MONO_LT_EQ" > "HOLLight.hollight.SQRT_MONO_LT_EQ"
  "SQRT_MONO_LT" > "HOLLight.hollight.SQRT_MONO_LT"
  "SQRT_MONO_LE_EQ" > "HOLLight.hollight.SQRT_MONO_LE_EQ"
  "SQRT_MONO_LE" > "HOLLight.hollight.SQRT_MONO_LE"
  "SQRT_INV" > "HOLLight.hollight.SQRT_INV"
  "SQRT_INJ" > "HOLLight.hollight.SQRT_INJ"
  "SQRT_EVEN_POW2" > "HOLLight.hollight.SQRT_EVEN_POW2"
  "SQRT_EQ_0" > "HOLLight.hollight.SQRT_EQ_0"
  "SQRT_DIV" > "HOLLight.hollight.SQRT_DIV"
  "SQRT_1" > "HOLLight.hollight.SQRT_1"
  "SQRT_0" > "HOLLight.hollight.SQRT_0"
  "SOME_def" > "HOLLight.hollight.SOME_def"
  "SNDCART_PASTECART" > "HOLLight.hollight.SNDCART_PASTECART"
  "SND" > "Product_Type.snd_conv"
  "SKOLEM_THM" > "HOLLight.hollight.SKOLEM_THM"
  "SIN_ZERO_PI" > "HOLLight.hollight.SIN_ZERO_PI"
  "SIN_ZERO_LEMMA" > "HOLLight.hollight.SIN_ZERO_LEMMA"
  "SIN_ZERO" > "HOLLight.hollight.SIN_ZERO"
  "SIN_TOTAL" > "HOLLight.hollight.SIN_TOTAL"
  "SIN_POS_PI_LE" > "HOLLight.hollight.SIN_POS_PI_LE"
  "SIN_POS_PI2" > "HOLLight.hollight.SIN_POS_PI2"
  "SIN_POS_PI" > "HOLLight.hollight.SIN_POS_PI"
  "SIN_POS" > "HOLLight.hollight.SIN_POS"
  "SIN_PI2" > "HOLLight.hollight.SIN_PI2"
  "SIN_PI" > "HOLLight.hollight.SIN_PI"
  "SIN_PERIODIC_PI" > "HOLLight.hollight.SIN_PERIODIC_PI"
  "SIN_PERIODIC" > "HOLLight.hollight.SIN_PERIODIC"
  "SIN_PAIRED" > "HOLLight.hollight.SIN_PAIRED"
  "SIN_NPI" > "HOLLight.hollight.SIN_NPI"
  "SIN_NEGLEMMA" > "HOLLight.hollight.SIN_NEGLEMMA"
  "SIN_NEG" > "HOLLight.hollight.SIN_NEG"
  "SIN_FDIFF" > "HOLLight.hollight.SIN_FDIFF"
  "SIN_DOUBLE" > "HOLLight.hollight.SIN_DOUBLE"
  "SIN_COS_SQRT" > "HOLLight.hollight.SIN_COS_SQRT"
  "SIN_COS_NEG" > "HOLLight.hollight.SIN_COS_NEG"
  "SIN_COS_ADD" > "HOLLight.hollight.SIN_COS_ADD"
  "SIN_COS" > "HOLLight.hollight.SIN_COS"
  "SIN_CONVERGES" > "HOLLight.hollight.SIN_CONVERGES"
  "SIN_CIRCLE" > "HOLLight.hollight.SIN_CIRCLE"
  "SIN_BOUNDS" > "HOLLight.hollight.SIN_BOUNDS"
  "SIN_BOUND" > "HOLLight.hollight.SIN_BOUND"
  "SIN_ASN" > "HOLLight.hollight.SIN_ASN"
  "SIN_ADD" > "HOLLight.hollight.SIN_ADD"
  "SIN_ACS_NZ" > "HOLLight.hollight.SIN_ACS_NZ"
  "SIN_0" > "HOLLight.hollight.SIN_0"
  "SING_def" > "HOLLight.hollight.SING_def"
  "SIMPLE_IMAGE" > "HOLLight.hollight.SIMPLE_IMAGE"
  "SET_RECURSION_LEMMA" > "HOLLight.hollight.SET_RECURSION_LEMMA"
  "SET_OF_LIST_OF_SET" > "HOLLight.hollight.SET_OF_LIST_OF_SET"
  "SET_OF_LIST_APPEND" > "HOLLight.hollight.SET_OF_LIST_APPEND"
  "SET_CASES" > "HOLLight.hollight.SET_CASES"
  "SETSPEC_def" > "HOLLight.hollight.SETSPEC_def"
  "SETOK_LE_LT" > "HOLLight.hollight.SETOK_LE_LT"
  "SER_ZERO" > "HOLLight.hollight.SER_ZERO"
  "SER_UNIQ" > "HOLLight.hollight.SER_UNIQ"
  "SER_SUB" > "HOLLight.hollight.SER_SUB"
  "SER_RATIO" > "HOLLight.hollight.SER_RATIO"
  "SER_POS_LT_PAIR" > "HOLLight.hollight.SER_POS_LT_PAIR"
  "SER_POS_LT" > "HOLLight.hollight.SER_POS_LT"
  "SER_POS_LE" > "HOLLight.hollight.SER_POS_LE"
  "SER_PAIR" > "HOLLight.hollight.SER_PAIR"
  "SER_OFFSET_REV" > "HOLLight.hollight.SER_OFFSET_REV"
  "SER_OFFSET" > "HOLLight.hollight.SER_OFFSET"
  "SER_NEG" > "HOLLight.hollight.SER_NEG"
  "SER_LE2" > "HOLLight.hollight.SER_LE2"
  "SER_LE" > "HOLLight.hollight.SER_LE"
  "SER_GROUP" > "HOLLight.hollight.SER_GROUP"
  "SER_COMPARA_UNIFORM_WEAK" > "HOLLight.hollight.SER_COMPARA_UNIFORM_WEAK"
  "SER_COMPARA_UNIFORM" > "HOLLight.hollight.SER_COMPARA_UNIFORM"
  "SER_COMPARA" > "HOLLight.hollight.SER_COMPARA"
  "SER_COMPAR" > "HOLLight.hollight.SER_COMPAR"
  "SER_CMUL" > "HOLLight.hollight.SER_CMUL"
  "SER_CDIV" > "HOLLight.hollight.SER_CDIV"
  "SER_CAUCHY" > "HOLLight.hollight.SER_CAUCHY"
  "SER_ADD" > "HOLLight.hollight.SER_ADD"
  "SER_ACONV" > "HOLLight.hollight.SER_ACONV"
  "SER_ABS" > "HOLLight.hollight.SER_ABS"
  "SER_0" > "HOLLight.hollight.SER_0"
  "SEQ_UNIQ" > "HOLLight.hollight.SEQ_UNIQ"
  "SEQ_TRUNCATION" > "HOLLight.hollight.SEQ_TRUNCATION"
  "SEQ_TRANSFORM" > "HOLLight.hollight.SEQ_TRANSFORM"
  "SEQ_TENDS" > "HOLLight.hollight.SEQ_TENDS"
  "SEQ_SUM" > "HOLLight.hollight.SEQ_SUM"
  "SEQ_SUC" > "HOLLight.hollight.SEQ_SUC"
  "SEQ_SUBLE" > "HOLLight.hollight.SEQ_SUBLE"
  "SEQ_SUB" > "HOLLight.hollight.SEQ_SUB"
  "SEQ_SBOUNDED" > "HOLLight.hollight.SEQ_SBOUNDED"
  "SEQ_POWER_ABS" > "HOLLight.hollight.SEQ_POWER_ABS"
  "SEQ_POWER" > "HOLLight.hollight.SEQ_POWER"
  "SEQ_NULL" > "HOLLight.hollight.SEQ_NULL"
  "SEQ_NPOW" > "HOLLight.hollight.SEQ_NPOW"
  "SEQ_NEG_CONV" > "HOLLight.hollight.SEQ_NEG_CONV"
  "SEQ_NEG_BOUNDED" > "HOLLight.hollight.SEQ_NEG_BOUNDED"
  "SEQ_NEG" > "HOLLight.hollight.SEQ_NEG"
  "SEQ_MUL" > "HOLLight.hollight.SEQ_MUL"
  "SEQ_MONOSUB" > "HOLLight.hollight.SEQ_MONOSUB"
  "SEQ_LIM" > "HOLLight.hollight.SEQ_LIM"
  "SEQ_LE_0" > "HOLLight.hollight.SEQ_LE_0"
  "SEQ_LE" > "HOLLight.hollight.SEQ_LE"
  "SEQ_INV0" > "HOLLight.hollight.SEQ_INV0"
  "SEQ_INV" > "HOLLight.hollight.SEQ_INV"
  "SEQ_ICONV" > "HOLLight.hollight.SEQ_ICONV"
  "SEQ_DIV" > "HOLLight.hollight.SEQ_DIV"
  "SEQ_DIRECT" > "HOLLight.hollight.SEQ_DIRECT"
  "SEQ_CONT_UNIFORM" > "HOLLight.hollight.SEQ_CONT_UNIFORM"
  "SEQ_CONST" > "HOLLight.hollight.SEQ_CONST"
  "SEQ_CBOUNDED" > "HOLLight.hollight.SEQ_CBOUNDED"
  "SEQ_CAUCHY" > "HOLLight.hollight.SEQ_CAUCHY"
  "SEQ_BOUNDED_2" > "HOLLight.hollight.SEQ_BOUNDED_2"
  "SEQ_BOUNDED" > "HOLLight.hollight.SEQ_BOUNDED"
  "SEQ_BCONV" > "HOLLight.hollight.SEQ_BCONV"
  "SEQ_ADD" > "HOLLight.hollight.SEQ_ADD"
  "SEQ_ABS_IMP" > "HOLLight.hollight.SEQ_ABS_IMP"
  "SEQ_ABS" > "HOLLight.hollight.SEQ_ABS"
  "SEQ" > "HOLLight.hollight.SEQ"
  "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"
  "ROOT_POW_POS" > "HOLLight.hollight.ROOT_POW_POS"
  "ROOT_POS_UNIQ" > "HOLLight.hollight.ROOT_POS_UNIQ"
  "ROOT_POS_POSITIVE" > "HOLLight.hollight.ROOT_POS_POSITIVE"
  "ROOT_MUL" > "HOLLight.hollight.ROOT_MUL"
  "ROOT_MONO_LT_EQ" > "HOLLight.hollight.ROOT_MONO_LT_EQ"
  "ROOT_MONO_LT" > "HOLLight.hollight.ROOT_MONO_LT"
  "ROOT_MONO_LE_EQ" > "HOLLight.hollight.ROOT_MONO_LE_EQ"
  "ROOT_MONO_LE" > "HOLLight.hollight.ROOT_MONO_LE"
  "ROOT_LT_LEMMA" > "HOLLight.hollight.ROOT_LT_LEMMA"
  "ROOT_LN" > "HOLLight.hollight.ROOT_LN"
  "ROOT_INV" > "HOLLight.hollight.ROOT_INV"
  "ROOT_INJ" > "HOLLight.hollight.ROOT_INJ"
  "ROOT_DIV" > "HOLLight.hollight.ROOT_DIV"
  "ROOT_1" > "HOLLight.hollight.ROOT_1"
  "ROOT_0" > "HOLLight.hollight.ROOT_0"
  "ROLLE" > "HOLLight.hollight.ROLLE"
  "RIGHT_SUB_DISTRIB" > "Nat.nat_distrib_3"
  "RIGHT_OR_FORALL_THM" > "HOL.all_simps_4"
  "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
  "RIGHT_OR_DISTRIB" > "HOL.conj_disj_distribR"
  "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" > "Nat.nat_distrib_1"
  "REVERSE_def" > "HOLLight.hollight.REVERSE_def"
  "REVERSE_REVERSE" > "HOLLight.hollight.REVERSE_REVERSE"
  "REVERSE_APPEND" > "HOLLight.hollight.REVERSE_APPEND"
  "REST_def" > "HOLLight.hollight.REST_def"
  "REP_ABS_PAIR" > "HOLLightCompat.REP_ABS_PAIR"
  "REPLICATE_def" > "HOLLight.hollight.REPLICATE_def"
  "REFL_CLAUSE" > "HOL.simp_thms_6"
  "RECURSION_CASEWISE_PAIRWISE" > "HOLLight.hollight.RECURSION_CASEWISE_PAIRWISE"
  "RECURSION_CASEWISE" > "HOLLight.hollight.RECURSION_CASEWISE"
  "REAL_WLOG_LT" > "HOLLight.hollight.REAL_WLOG_LT"
  "REAL_WLOG_LE" > "HOLLight.hollight.REAL_WLOG_LE"
  "REAL_SUP_UBOUND_LE" > "HOLLight.hollight.REAL_SUP_UBOUND_LE"
  "REAL_SUP_UBOUND" > "HOLLight.hollight.REAL_SUP_UBOUND"
  "REAL_SUP_LE" > "HOLLight.hollight.REAL_SUP_LE"
  "REAL_SUP_EXISTS" > "HOLLight.hollight.REAL_SUP_EXISTS"
  "REAL_SUP" > "HOLLight.hollight.REAL_SUP"
  "REAL_SUMSQ" > "HOLLight.hollight.REAL_SUMSQ"
  "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_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_INV2" > "HOLLight.hollight.REAL_SUB_INV2"
  "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_RNEG_UNIQ" > "HOLLight.hollight.REAL_RNEG_UNIQ"
  "REAL_RINV_UNIQ" > "HOLLight.hollight.REAL_RINV_UNIQ"
  "REAL_RDISTRIB" > "HOLLight.hollight.REAL_RDISTRIB"
  "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" > "HOLLight.hollight.REAL_POW_MONO"
  "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" > "HOLLight.hollight.REAL_POW_LE2"
  "REAL_POW_LE" > "HOLLight.hollight.REAL_POW_LE"
  "REAL_POW_INV" > "HOLLight.hollight.REAL_POW_INV"
  "REAL_POW_EQ_0" > "HOLLight.hollight.REAL_POW_EQ_0"
  "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_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_POSSQ" > "HOLLight.hollight.REAL_POSSQ"
  "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_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_NZ_IMP_LT" > "HOLLight.hollight.REAL_NZ_IMP_LT"
  "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_INV" > "HOLLight.hollight.REAL_NEG_INV"
  "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_EQ0" > "HOLLight.hollight.REAL_NEG_EQ0"
  "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_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_MUL" > "HOLLight.hollight.REAL_MUL"
  "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_MIDDLE2" > "HOLLight.hollight.REAL_MIDDLE2"
  "REAL_MIDDLE1" > "HOLLight.hollight.REAL_MIDDLE1"
  "REAL_MEAN" > "HOLLight.hollight.REAL_MEAN"
  "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" > "HOLLight.hollight.REAL_LT_SQUARE"
  "REAL_LT_RNEG" > "HOLLight.hollight.REAL_LT_RNEG"
  "REAL_LT_RMUL_IMP" > "HOLLight.hollight.REAL_LT_RMUL_IMP"
  "REAL_LT_RMUL_EQ" > "HOLLight.hollight.REAL_LT_RMUL_EQ"
  "REAL_LT_RMUL_0" > "HOLLight.hollight.REAL_LT_RMUL_0"
  "REAL_LT_RMUL" > "HOLLight.hollight.REAL_LT_RMUL"
  "REAL_LT_REFL" > "HOLLight.hollight.REAL_LT_REFL"
  "REAL_LT_RDIV_EQ" > "HOLLight.hollight.REAL_LT_RDIV_EQ"
  "REAL_LT_RDIV_0" > "HOLLight.hollight.REAL_LT_RDIV_0"
  "REAL_LT_RDIV" > "HOLLight.hollight.REAL_LT_RDIV"
  "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_NZ" > "HOLLight.hollight.REAL_LT_NZ"
  "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_MULTIPLE" > "HOLLight.hollight.REAL_LT_MULTIPLE"
  "REAL_LT_MUL2_ALT" > "HOLLight.hollight.REAL_LT_MUL2_ALT"
  "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_IMP" > "HOLLight.hollight.REAL_LT_LMUL_IMP"
  "REAL_LT_LMUL_EQ" > "HOLLight.hollight.REAL_LT_LMUL_EQ"
  "REAL_LT_LMUL_0" > "HOLLight.hollight.REAL_LT_LMUL_0"
  "REAL_LT_LMUL" > "HOLLight.hollight.REAL_LT_LMUL"
  "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_HALF2" > "HOLLight.hollight.REAL_LT_HALF2"
  "REAL_LT_HALF1" > "HOLLight.hollight.REAL_LT_HALF1"
  "REAL_LT_GT" > "HOLLight.hollight.REAL_LT_GT"
  "REAL_LT_FRACTION_0" > "HOLLight.hollight.REAL_LT_FRACTION_0"
  "REAL_LT_FRACTION" > "HOLLight.hollight.REAL_LT_FRACTION"
  "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_1" > "HOLLight.hollight.REAL_LT_1"
  "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_LT1_POW2" > "HOLLight.hollight.REAL_LT1_POW2"
  "REAL_LT" > "HOLLight.hollight.REAL_LT"
  "REAL_LNEG_UNIQ" > "HOLLight.hollight.REAL_LNEG_UNIQ"
  "REAL_LINV_UNIQ" > "HOLLight.hollight.REAL_LINV_UNIQ"
  "REAL_LE_TRANS" > "HOLLight.hollight.REAL_LE_TRANS"
  "REAL_LE_TOTAL" > "HOLLight.hollight.REAL_LE_TOTAL"
  "REAL_LE_SUB_RADD" > "HOLLight.hollight.REAL_LE_SUB_RADD"
  "REAL_LE_SUB_LADD" > "HOLLight.hollight.REAL_LE_SUB_LADD"
  "REAL_LE_SQUARE_POW" > "HOLLight.hollight.REAL_LE_SQUARE_POW"
  "REAL_LE_SQUARE_ABS" > "HOLLight.hollight.REAL_LE_SQUARE_ABS"
  "REAL_LE_SQUARE" > "HOLLight.hollight.REAL_LE_SQUARE"
  "REAL_LE_RSQRT" > "HOLLight.hollight.REAL_LE_RSQRT"
  "REAL_LE_RNEG" > "HOLLight.hollight.REAL_LE_RNEG"
  "REAL_LE_RMUL_IMP" > "HOLLight.hollight.REAL_LE_RMUL_IMP"
  "REAL_LE_RMUL_EQ" > "HOLLight.hollight.REAL_LE_RMUL_EQ"
  "REAL_LE_RMUL" > "HOLLight.hollight.REAL_LE_RMUL"
  "REAL_LE_REFL" > "HOLLight.hollight.REAL_LE_REFL"
  "REAL_LE_RDIV_EQ" > "HOLLight.hollight.REAL_LE_RDIV_EQ"
  "REAL_LE_RDIV" > "HOLLight.hollight.REAL_LE_RDIV"
  "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_MUL2V" > "HOLLight.hollight.REAL_LE_MUL2V"
  "REAL_LE_MUL2" > "HOLLight.hollight.REAL_LE_MUL2"
  "REAL_LE_MUL" > "HOLLight.hollight.REAL_LE_MUL"
  "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_LSQRT" > "HOLLight.hollight.REAL_LE_LSQRT"
  "REAL_LE_LNEG" > "HOLLight.hollight.REAL_LE_LNEG"
  "REAL_LE_LMUL_LOCAL" > "HOLLight.hollight.REAL_LE_LMUL_LOCAL"
  "REAL_LE_LMUL_IMP" > "HOLLight.hollight.REAL_LE_LMUL_IMP"
  "REAL_LE_LMUL_EQ" > "HOLLight.hollight.REAL_LE_LMUL_EQ"
  "REAL_LE_LMUL" > "HOLLight.hollight.REAL_LE_LMUL"
  "REAL_LE_LDIV_EQ" > "HOLLight.hollight.REAL_LE_LDIV_EQ"
  "REAL_LE_LDIV" > "HOLLight.hollight.REAL_LE_LDIV"
  "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_ANTISYM" > "HOLLight.hollight.REAL_LE_ANTISYM"
  "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_LE1_POW2" > "HOLLight.hollight.REAL_LE1_POW2"
  "REAL_LE" > "HOLLight.hollight.REAL_LE"
  "REAL_INV_POS" > "HOLLight.hollight.REAL_INV_POS"
  "REAL_INV_NZ" > "HOLLight.hollight.REAL_INV_NZ"
  "REAL_INV_NEG" > "HOLLight.hollight.REAL_INV_NEG"
  "REAL_INV_MUL_WEAK" > "HOLLight.hollight.REAL_INV_MUL_WEAK"
  "REAL_INV_MUL" > "HOLLight.hollight.REAL_INV_MUL"
  "REAL_INV_LT1" > "HOLLight.hollight.REAL_INV_LT1"
  "REAL_INV_LE_1" > "HOLLight.hollight.REAL_INV_LE_1"
  "REAL_INV_INV" > "HOLLight.hollight.REAL_INV_INV"
  "REAL_INV_EQ_0" > "HOLLight.hollight.REAL_INV_EQ_0"
  "REAL_INV_DIV" > "HOLLight.hollight.REAL_INV_DIV"
  "REAL_INV_1_LE" > "HOLLight.hollight.REAL_INV_1_LE"
  "REAL_INV_1OVER" > "HOLLight.hollight.REAL_INV_1OVER"
  "REAL_INV_1" > "HOLLight.hollight.REAL_INV_1"
  "REAL_INVINV" > "HOLLight.hollight.REAL_INVINV"
  "REAL_INV1" > "HOLLight.hollight.REAL_INV1"
  "REAL_INJ" > "HOLLight.hollight.REAL_INJ"
  "REAL_HREAL_LEMMA2" > "HOLLight.hollight.REAL_HREAL_LEMMA2"
  "REAL_HREAL_LEMMA1" > "HOLLight.hollight.REAL_HREAL_LEMMA1"
  "REAL_HALF_DOUBLE" > "HOLLight.hollight.REAL_HALF_DOUBLE"
  "REAL_FACT_NZ" > "HOLLight.hollight.REAL_FACT_NZ"
  "REAL_EXP_TOTAL_LEMMA" > "HOLLight.hollight.REAL_EXP_TOTAL_LEMMA"
  "REAL_EXP_TOTAL" > "HOLLight.hollight.REAL_EXP_TOTAL"
  "REAL_EXP_SUB" > "HOLLight.hollight.REAL_EXP_SUB"
  "REAL_EXP_POS_LT" > "HOLLight.hollight.REAL_EXP_POS_LT"
  "REAL_EXP_POS_LE" > "HOLLight.hollight.REAL_EXP_POS_LE"
  "REAL_EXP_NZ" > "HOLLight.hollight.REAL_EXP_NZ"
  "REAL_EXP_NEG_MUL2" > "HOLLight.hollight.REAL_EXP_NEG_MUL2"
  "REAL_EXP_NEG_MUL" > "HOLLight.hollight.REAL_EXP_NEG_MUL"
  "REAL_EXP_NEG" > "HOLLight.hollight.REAL_EXP_NEG"
  "REAL_EXP_N" > "HOLLight.hollight.REAL_EXP_N"
  "REAL_EXP_MONO_LT" > "HOLLight.hollight.REAL_EXP_MONO_LT"
  "REAL_EXP_MONO_LE" > "HOLLight.hollight.REAL_EXP_MONO_LE"
  "REAL_EXP_MONO_IMP" > "HOLLight.hollight.REAL_EXP_MONO_IMP"
  "REAL_EXP_LT_1" > "HOLLight.hollight.REAL_EXP_LT_1"
  "REAL_EXP_LN" > "HOLLight.hollight.REAL_EXP_LN"
  "REAL_EXP_LE_X" > "HOLLight.hollight.REAL_EXP_LE_X"
  "REAL_EXP_INJ" > "HOLLight.hollight.REAL_EXP_INJ"
  "REAL_EXP_FDIFF" > "HOLLight.hollight.REAL_EXP_FDIFF"
  "REAL_EXP_CONVERGES" > "HOLLight.hollight.REAL_EXP_CONVERGES"
  "REAL_EXP_BOUND_LEMMA" > "HOLLight.hollight.REAL_EXP_BOUND_LEMMA"
  "REAL_EXP_ADD_MUL" > "HOLLight.hollight.REAL_EXP_ADD_MUL"
  "REAL_EXP_ADD" > "HOLLight.hollight.REAL_EXP_ADD"
  "REAL_EXP_0" > "HOLLight.hollight.REAL_EXP_0"
  "REAL_EQ_SUB_RADD" > "HOLLight.hollight.REAL_EQ_SUB_RADD"
  "REAL_EQ_SUB_LADD" > "HOLLight.hollight.REAL_EQ_SUB_LADD"
  "REAL_EQ_RMUL_IMP" > "HOLLight.hollight.REAL_EQ_RMUL_IMP"
  "REAL_EQ_RMUL" > "HOLLight.hollight.REAL_EQ_RMUL"
  "REAL_EQ_RDIV_EQ" > "HOLLight.hollight.REAL_EQ_RDIV_EQ"
  "REAL_EQ_RCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_RCANCEL_IMP"
  "REAL_EQ_RADD" > "HOLLight.hollight.REAL_EQ_RADD"
  "REAL_EQ_NEG2" > "HOLLight.hollight.REAL_EQ_NEG2"
  "REAL_EQ_NEG" > "HOLLight.hollight.REAL_EQ_NEG"
  "REAL_EQ_MUL_RCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_RCANCEL"
  "REAL_EQ_MUL_LCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_LCANCEL"
  "REAL_EQ_LMUL_IMP" > "HOLLight.hollight.REAL_EQ_LMUL_IMP"
  "REAL_EQ_LMUL2" > "HOLLight.hollight.REAL_EQ_LMUL2"
  "REAL_EQ_LMUL" > "HOLLight.hollight.REAL_EQ_LMUL"
  "REAL_EQ_LDIV_EQ" > "HOLLight.hollight.REAL_EQ_LDIV_EQ"
  "REAL_EQ_LCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_LCANCEL_IMP"
  "REAL_EQ_LADD" > "HOLLight.hollight.REAL_EQ_LADD"
  "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_DOUBLE" > "HOLLight.hollight.REAL_DOUBLE"
  "REAL_DIV_SQRT" > "HOLLight.hollight.REAL_DIV_SQRT"
  "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_MUL2" > "HOLLight.hollight.REAL_DIV_MUL2"
  "REAL_DIV_LZERO" > "HOLLight.hollight.REAL_DIV_LZERO"
  "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_ATN_POWSER_SUMMABLE" > "HOLLight.hollight.REAL_ATN_POWSER_SUMMABLE"
  "REAL_ATN_POWSER_DIFFS_SUMMABLE" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFS_SUMMABLE"
  "REAL_ATN_POWSER_DIFFS_SUM" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFS_SUM"
  "REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFS_DIFFS_SUMMABLE"
  "REAL_ATN_POWSER_DIFFL" > "HOLLight.hollight.REAL_ATN_POWSER_DIFFL"
  "REAL_ATN_POWSER" > "HOLLight.hollight.REAL_ATN_POWSER"
  "REAL_ARCH_SIMPLE" > "HOLLight.hollight.REAL_ARCH_SIMPLE"
  "REAL_ARCH_LEAST" > "HOLLight.hollight.REAL_ARCH_LEAST"
  "REAL_ARCH" > "HOLLight.hollight.REAL_ARCH"
  "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_UNIQ" > "HOLLight.hollight.REAL_ADD_RID_UNIQ"
  "REAL_ADD_RID" > "HOLLight.hollight.REAL_ADD_RID"
  "REAL_ADD_RDISTRIB" > "HOLLight.hollight.REAL_ADD_RDISTRIB"
  "REAL_ADD_LID_UNIQ" > "HOLLight.hollight.REAL_ADD_LID_UNIQ"
  "REAL_ADD_AC" > "HOLLight.hollight.REAL_ADD_AC"
  "REAL_ADD2_SUB2" > "HOLLight.hollight.REAL_ADD2_SUB2"
  "REAL_ADD" > "HOLLight.hollight.REAL_ADD"
  "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_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"
  "REAL" > "HOLLight.hollight.REAL"
  "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"
  "PSUM_SUM_NUMSEG" > "HOLLight.hollight.PSUM_SUM_NUMSEG"
  "PSUM_SUM" > "HOLLight.hollight.PSUM_SUM"
  "PSUBSET_def" > "HOLLight.hollight.PSUBSET_def"
  "PSUBSET_UNIV" > "HOLLight.hollight.PSUBSET_UNIV"
  "PSUBSET_TRANS" > "HOLLight.hollight.PSUBSET_TRANS"
  "PSUBSET_SUBSET_TRANS" > "HOLLight.hollight.PSUBSET_SUBSET_TRANS"
  "PSUBSET_MEMBER" > "HOLLight.hollight.PSUBSET_MEMBER"
  "PSUBSET_IRREFL" > "HOLLight.hollight.PSUBSET_IRREFL"
  "PSUBSET_INSERT_SUBSET" > "HOLLight.hollight.PSUBSET_INSERT_SUBSET"
  "PRE_ELIM_THM" > "HOLLight.hollight.PRE_ELIM_THM"
  "POW_ZERO_EQ" > "HOLLight.hollight.POW_ZERO_EQ"
  "POW_ZERO" > "HOLLight.hollight.POW_ZERO"
  "POW_ROOT_POS" > "HOLLight.hollight.POW_ROOT_POS"
  "POW_POS_LT" > "HOLLight.hollight.POW_POS_LT"
  "POW_POS" > "HOLLight.hollight.POW_POS"
  "POW_PLUS1" > "HOLLight.hollight.POW_PLUS1"
  "POW_NZ" > "HOLLight.hollight.POW_NZ"
  "POW_MUL" > "HOLLight.hollight.POW_MUL"
  "POW_MINUS1" > "HOLLight.hollight.POW_MINUS1"
  "POW_M1" > "HOLLight.hollight.POW_M1"
  "POW_LT" > "HOLLight.hollight.POW_LT"
  "POW_LE" > "HOLLight.hollight.POW_LE"
  "POW_INV" > "HOLLight.hollight.POW_INV"
  "POW_EQ" > "HOLLight.hollight.POW_EQ"
  "POW_ADD" > "HOLLight.hollight.POW_ADD"
  "POW_ABS" > "HOLLight.hollight.POW_ABS"
  "POW_2_SQRT_ABS" > "HOLLight.hollight.POW_2_SQRT_ABS"
  "POW_2_SQRT" > "HOLLight.hollight.POW_2_SQRT"
  "POW_2_LT" > "HOLLight.hollight.POW_2_LT"
  "POW_2_LE1" > "HOLLight.hollight.POW_2_LE1"
  "POW_2" > "HOLLight.hollight.POW_2"
  "POW_1" > "HOLLight.hollight.POW_1"
  "POW_0" > "HOLLight.hollight.POW_0"
  "POWSER_LIMIT_0_STRONG" > "HOLLight.hollight.POWSER_LIMIT_0_STRONG"
  "POWSER_LIMIT_0" > "HOLLight.hollight.POWSER_LIMIT_0"
  "POWSER_INSIDEA" > "HOLLight.hollight.POWSER_INSIDEA"
  "POWSER_INSIDE" > "HOLLight.hollight.POWSER_INSIDE"
  "POWSER_EQUAL_0" > "HOLLight.hollight.POWSER_EQUAL_0"
  "POWSER_EQUAL" > "HOLLight.hollight.POWSER_EQUAL"
  "POWSER_0" > "HOLLight.hollight.POWSER_0"
  "POWREV" > "HOLLight.hollight.POWREV"
  "POWDIFF_LEMMA" > "HOLLight.hollight.POWDIFF_LEMMA"
  "POWDIFF" > "HOLLight.hollight.POWDIFF"
  "PI_POS" > "HOLLight.hollight.PI_POS"
  "PI2_PI4" > "HOLLight.hollight.PI2_PI4"
  "PI2_BOUNDS" > "HOLLight.hollight.PI2_BOUNDS"
  "PI2" > "HOLLight.hollight.PI2"
  "PASTECART_FST_SND" > "HOLLight.hollight.PASTECART_FST_SND"
  "PASTECART_EQ" > "HOLLight.hollight.PASTECART_EQ"
  "PASSOC_def" > "HOLLight.hollight.PASSOC_def"
  "PAIR_SURJECTIVE" > "Datatype.prod.nchotomy"
  "PAIR_EXISTS_THM" > "HOLLight.hollight.PAIR_EXISTS_THM"
  "PAIR_EQ" > "Datatype.prod.simps_1"
  "PAIRWISE_def" > "HOLLight.hollight.PAIRWISE_def"
  "PAIR" > "HOL4Compat.PAIR"
  "OUTR_def" > "HOLLight.hollight.OUTR_def"
  "OUTL_def" > "HOLLight.hollight.OUTL_def"
  "OR_EXISTS_THM" > "HOL.ex_disj_distrib"
  "OR_CLAUSES" > "HOLLight.hollight.OR_CLAUSES"
  "OPEN_UNOPEN" > "HOLLight.hollight.OPEN_UNOPEN"
  "OPEN_SUBOPEN" > "HOLLight.hollight.OPEN_SUBOPEN"
  "OPEN_OWN_NEIGH" > "HOLLight.hollight.OPEN_OWN_NEIGH"
  "OPEN_NEIGH" > "HOLLight.hollight.OPEN_NEIGH"
  "ONE" > "HOLLight.hollight.ONE"
  "ODD_def" > "HOLLight.hollight.ODD_def"
  "ODD_MULT" > "HOLLight.hollight.ODD_MULT"
  "ODD_MOD" > "HOLLight.hollight.ODD_MOD"
  "ODD_EXP" > "HOLLight.hollight.ODD_EXP"
  "ODD_EXISTS" > "HOLLight.hollight.ODD_EXISTS"
  "ODD_DOUBLE" > "HOLLight.hollight.ODD_DOUBLE"
  "ODD_ADD" > "HOLLight.hollight.ODD_ADD"
  "NUM_INTEGRAL_LEMMA" > "HOLLight.hollight.NUM_INTEGRAL_LEMMA"
  "NUM_INTEGRAL" > "HOLLight.hollight.NUM_INTEGRAL"
  "NUMSUM_def" > "HOLLight.hollight.NUMSUM_def"
  "NUMSUM_INJ" > "HOLLight.hollight.NUMSUM_INJ"
  "NUMSND_def" > "HOLLight.hollight.NUMSND_def"
  "NUMSEG_SING" > "HOLLight.hollight.NUMSEG_SING"
  "NUMSEG_RREC" > "HOLLight.hollight.NUMSEG_RREC"
  "NUMSEG_REC" > "HOLLight.hollight.NUMSEG_REC"
  "NUMSEG_OFFSET_IMAGE" > "HOLLight.hollight.NUMSEG_OFFSET_IMAGE"
  "NUMSEG_LREC" > "HOLLight.hollight.NUMSEG_LREC"
  "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"
  "NULL_def" > "HOLLight.hollight.NULL_def"
  "NSUM_UNION_RZERO" > "HOLLight.hollight.NSUM_UNION_RZERO"
  "NSUM_UNION_LZERO" > "HOLLight.hollight.NSUM_UNION_LZERO"
  "NSUM_UNION_EQ" > "HOLLight.hollight.NSUM_UNION_EQ"
  "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_RESTRICT_SET" > "HOLLight.hollight.NSUM_RESTRICT_SET"
  "NSUM_RESTRICT" > "HOLLight.hollight.NSUM_RESTRICT"
  "NSUM_POS_LE_NUMSEG" > "HOLLight.hollight.NSUM_POS_LE_NUMSEG"
  "NSUM_POS_LE" > "HOLLight.hollight.NSUM_POS_LE"
  "NSUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_POS_EQ_0_NUMSEG"
  "NSUM_POS_EQ_0" > "HOLLight.hollight.NSUM_POS_EQ_0"
  "NSUM_POS_BOUND" > "HOLLight.hollight.NSUM_POS_BOUND"
  "NSUM_OFFSET_0" > "HOLLight.hollight.NSUM_OFFSET_0"
  "NSUM_OFFSET" > "HOLLight.hollight.NSUM_OFFSET"
  "NSUM_NSUM_RESTRICT" > "HOLLight.hollight.NSUM_NSUM_RESTRICT"
  "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_LE_NUMSEG" > "HOLLight.hollight.NSUM_LE_NUMSEG"
  "NSUM_LE" > "HOLLight.hollight.NSUM_LE"
  "NSUM_IMAGE_GEN" > "HOLLight.hollight.NSUM_IMAGE_GEN"
  "NSUM_IMAGE" > "HOLLight.hollight.NSUM_IMAGE"
  "NSUM_EQ_SUPERSET" > "HOLLight.hollight.NSUM_EQ_SUPERSET"
  "NSUM_EQ_NUMSEG" > "HOLLight.hollight.NSUM_EQ_NUMSEG"
  "NSUM_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_NUMSEG"
  "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_CONST_NUMSEG" > "HOLLight.hollight.NSUM_CONST_NUMSEG"
  "NSUM_CONST" > "HOLLight.hollight.NSUM_CONST"
  "NSUM_CMUL_NUMSEG" > "HOLLight.hollight.NSUM_CMUL_NUMSEG"
  "NSUM_CMUL" > "HOLLight.hollight.NSUM_CMUL"
  "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_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_ADD_SPLIT" > "HOLLight.hollight.NSUM_ADD_SPLIT"
  "NSUM_ADD_NUMSEG" > "HOLLight.hollight.NSUM_ADD_NUMSEG"
  "NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
  "NSUM_0" > "HOLLight.hollight.NSUM_0"
  "NOT_UNIV_PSUBSET" > "HOLLight.hollight.NOT_UNIV_PSUBSET"
  "NOT_SUC" > "Nat.nat.simps_1"
  "NOT_PSUBSET_EMPTY" > "HOLLight.hollight.NOT_PSUBSET_EMPTY"
  "NOT_ODD" > "HOLLight.hollight.NOT_ODD"
  "NOT_LT" > "HOLLight.hollight.NOT_LT"
  "NOT_LE" > "HOLLight.hollight.NOT_LE"
  "NOT_IN_EMPTY" > "HOLLight.hollight.NOT_IN_EMPTY"
  "NOT_INSERT_EMPTY" > "HOLLight.hollight.NOT_INSERT_EMPTY"
  "NOT_FORALL_THM" > "Inductive.basic_monos_15"
  "NOT_EXISTS_THM" > "Inductive.basic_monos_16"
  "NOT_EX" > "HOLLight.hollight.NOT_EX"
  "NOT_EVEN" > "HOLLight.hollight.NOT_EVEN"
  "NOT_EQUAL_SETS" > "HOLLight.hollight.NOT_EQUAL_SETS"
  "NOT_EMPTY_INSERT" > "HOLLight.hollight.NOT_EMPTY_INSERT"
  "NOT_CONS_NIL" > "HOLLight.hollight.NOT_CONS_NIL"
  "NOT_CLAUSES_WEAK" > "HOLLight.hollight.NOT_CLAUSES_WEAK"
  "NOT_ALL" > "HOLLight.hollight.NOT_ALL"
  "NONE_def" > "HOLLight.hollight.NONE_def"
  "NIL_def" > "HOLLight.hollight.NIL_def"
  "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"
  "NET_SUM" > "HOLLight.hollight.NET_SUM"
  "NET_SUB" > "HOLLight.hollight.NET_SUB"
  "NET_NULL_MUL" > "HOLLight.hollight.NET_NULL_MUL"
  "NET_NULL_CMUL" > "HOLLight.hollight.NET_NULL_CMUL"
  "NET_NULL_ADD" > "HOLLight.hollight.NET_NULL_ADD"
  "NET_NULL" > "HOLLight.hollight.NET_NULL"
  "NET_NEG" > "HOLLight.hollight.NET_NEG"
  "NET_MUL" > "HOLLight.hollight.NET_MUL"
  "NET_LE" > "HOLLight.hollight.NET_LE"
  "NET_INV" > "HOLLight.hollight.NET_INV"
  "NET_DIV" > "HOLLight.hollight.NET_DIV"
  "NET_CONV_NZ" > "HOLLight.hollight.NET_CONV_NZ"
  "NET_CONV_IBOUNDED" > "HOLLight.hollight.NET_CONV_IBOUNDED"
  "NET_CONV_BOUNDED" > "HOLLight.hollight.NET_CONV_BOUNDED"
  "NET_ADD" > "HOLLight.hollight.NET_ADD"
  "NET_ABS" > "HOLLight.hollight.NET_ABS"
  "NEST_LEMMA_UNIQ" > "HOLLight.hollight.NEST_LEMMA_UNIQ"
  "NEST_LEMMA" > "HOLLight.hollight.NEST_LEMMA"
  "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"
  "MVT_LEMMA" > "HOLLight.hollight.MVT_LEMMA"
  "MVT_ALT" > "HOLLight.hollight.MVT_ALT"
  "MVT" > "HOLLight.hollight.MVT"
  "MULT_SYM" > "IntDef.zmult_ac_2"
  "MULT_SUC" > "Nat.mult_Suc_right"
  "MULT_EXP" > "HOLLight.hollight.MULT_EXP"
  "MULT_EQ_1" > "HOLLight.hollight.MULT_EQ_1"
  "MULT_EQ_0" > "Nat.mult_is_0"
  "MULT_DIV_2" > "HOLLight.hollight.MULT_DIV_2"
  "MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
  "MULT_ASSOC" > "IntDef.zmult_ac_1"
  "MULT_AC" > "HOLLight.hollight.MULT_AC"
  "MULT_2" > "HOLLight.hollight.MULT_2"
  "MULT_0" > "Nat.mult_0_right"
  "MTOP_TENDS_UNIQ" > "HOLLight.hollight.MTOP_TENDS_UNIQ"
  "MTOP_TENDS" > "HOLLight.hollight.MTOP_TENDS"
  "MTOP_OPEN" > "HOLLight.hollight.MTOP_OPEN"
  "MTOP_LIMPT" > "HOLLight.hollight.MTOP_LIMPT"
  "MR1_SUB_LT" > "HOLLight.hollight.MR1_SUB_LT"
  "MR1_SUB_LE" > "HOLLight.hollight.MR1_SUB_LE"
  "MR1_SUB" > "HOLLight.hollight.MR1_SUB"
  "MR1_LIMPT" > "HOLLight.hollight.MR1_LIMPT"
  "MR1_DEF" > "HOLLight.hollight.MR1_DEF"
  "MR1_BOUNDED" > "HOLLight.hollight.MR1_BOUNDED"
  "MR1_BETWEEN1" > "HOLLight.hollight.MR1_BETWEEN1"
  "MR1_ADD_LT" > "HOLLight.hollight.MR1_ADD_LT"
  "MR1_ADD_LE" > "HOLLight.hollight.MR1_ADD_LE"
  "MR1_ADD" > "HOLLight.hollight.MR1_ADD"
  "MONO_SUC" > "HOLLight.hollight.MONO_SUC"
  "MONO_FORALL" > "Inductive.basic_monos_6"
  "MONO_EXISTS" > "Inductive.basic_monos_5"
  "MONO_COND" > "HOLLight.hollight.MONO_COND"
  "MONO_ALL2" > "HOLLight.hollight.MONO_ALL2"
  "MONO_ALL" > "HOLLight.hollight.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"
  "MOD_def" > "HOLLight.hollight.MOD_def"
  "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" > "HOLLight.hollight.MOD_MULT_ADD"
  "MOD_MULT2" > "HOLLight.hollight.MOD_MULT2"
  "MOD_MULT" > "HOLLight.hollight.MOD_MULT"
  "MOD_MOD_REFL" > "HOLLight.hollight.MOD_MOD_REFL"
  "MOD_MOD" > "HOLLight.hollight.MOD_MOD"
  "MOD_LT" > "HOLLight.hollight.MOD_LT"
  "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"
  "MOD_1" > "HOLLight.hollight.MOD_1"
  "MOD_0" > "HOLLight.hollight.MOD_0"
  "MK_REC_INJ" > "HOLLight.hollight.MK_REC_INJ"
  "MINIMAL" > "HOLLight.hollight.MINIMAL"
  "METRIC_ZERO" > "HOLLight.hollight.METRIC_ZERO"
  "METRIC_TRIANGLE" > "HOLLight.hollight.METRIC_TRIANGLE"
  "METRIC_SYM" > "HOLLight.hollight.METRIC_SYM"
  "METRIC_SAME" > "HOLLight.hollight.METRIC_SAME"
  "METRIC_POS" > "HOLLight.hollight.METRIC_POS"
  "METRIC_NZ" > "HOLLight.hollight.METRIC_NZ"
  "METRIC_ISMET" > "HOLLight.hollight.METRIC_ISMET"
  "MEM_def" > "HOLLight.hollight.MEM_def"
  "MEM_MAP" > "HOLLight.hollight.MEM_MAP"
  "MEM_LIST_OF_SET" > "HOLLight.hollight.MEM_LIST_OF_SET"
  "MEM_FILTER" > "HOLLight.hollight.MEM_FILTER"
  "MEM_EL" > "HOLLight.hollight.MEM_EL"
  "MEM_ASSOC" > "HOLLight.hollight.MEM_ASSOC"
  "MEM_APPEND" > "HOLLight.hollight.MEM_APPEND"
  "MEMBER_NOT_EMPTY" > "HOLLight.hollight.MEMBER_NOT_EMPTY"
  "MEASURE_LE" > "HOLLight.hollight.MEASURE_LE"
  "MCLAURIN_ZERO" > "HOLLight.hollight.MCLAURIN_ZERO"
  "MCLAURIN_SIN" > "HOLLight.hollight.MCLAURIN_SIN"
  "MCLAURIN_NEG" > "HOLLight.hollight.MCLAURIN_NEG"
  "MCLAURIN_LN_POS" > "HOLLight.hollight.MCLAURIN_LN_POS"
  "MCLAURIN_LN_NEG" > "HOLLight.hollight.MCLAURIN_LN_NEG"
  "MCLAURIN_EXP_LT" > "HOLLight.hollight.MCLAURIN_EXP_LT"
  "MCLAURIN_EXP_LEMMA" > "HOLLight.hollight.MCLAURIN_EXP_LEMMA"
  "MCLAURIN_EXP_LE" > "HOLLight.hollight.MCLAURIN_EXP_LE"
  "MCLAURIN_COS" > "HOLLight.hollight.MCLAURIN_COS"
  "MCLAURIN_BI_LE" > "HOLLight.hollight.MCLAURIN_BI_LE"
  "MCLAURIN_ATN" > "HOLLight.hollight.MCLAURIN_ATN"
  "MCLAURIN_ALL_LT" > "HOLLight.hollight.MCLAURIN_ALL_LT"
  "MCLAURIN_ALL_LE" > "HOLLight.hollight.MCLAURIN_ALL_LE"
  "MCLAURIN" > "HOLLight.hollight.MCLAURIN"
  "MAX_LEMMA" > "HOLLight.hollight.MAX_LEMMA"
  "MAP_o" > "HOLLight.hollight.MAP_o"
  "MAP_def" > "HOLLight.hollight.MAP_def"
  "MAP_SND_ZIP" > "HOLLight.hollight.MAP_SND_ZIP"
  "MAP_FST_ZIP" > "HOLLight.hollight.MAP_FST_ZIP"
  "MAP_EQ_DEGEN" > "HOLLight.hollight.MAP_EQ_DEGEN"
  "MAP_EQ_ALL2" > "HOLLight.hollight.MAP_EQ_ALL2"
  "MAP_EQ" > "HOLLight.hollight.MAP_EQ"
  "MAP_APPEND" > "HOLLight.hollight.MAP_APPEND"
  "MAP2_def" > "HOLLight.hollight.MAP2_def"
  "MAP2" > "HOLLight.hollight.MAP2"
  "LT_TRANS" > "HOLLight.hollight.LT_TRANS"
  "LT_SUC_LE" > "HOLLight.hollight.LT_SUC_LE"
  "LT_SUC" > "HOLLight.hollight.LT_SUC"
  "LT_REFL" > "HOLLight.hollight.LT_REFL"
  "LT_NZ" > "HOLLight.hollight.LT_NZ"
  "LT_MULT_RCANCEL" > "HOLLight.hollight.LT_MULT_RCANCEL"
  "LT_MULT_LCANCEL" > "HOLLight.hollight.LT_MULT_LCANCEL"
  "LT_MULT2" > "HOLLight.hollight.LT_MULT2"
  "LT_MULT" > "HOLLight.hollight.LT_MULT"
  "LT_LMULT" > "HOLLight.hollight.LT_LMULT"
  "LT_LE" > "HOLLight.hollight.LT_LE"
  "LT_IMP_LE" > "HOLLight.hollight.LT_IMP_LE"
  "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" > "HOLLight.hollight.LT_ADD_RCANCEL"
  "LT_ADD_LCANCEL" > "HOLLight.hollight.LT_ADD_LCANCEL"
  "LT_ADDR" > "HOLLight.hollight.LT_ADDR"
  "LT_ADD2" > "HOLLight.hollight.LT_ADD2"
  "LT_ADD" > "HOLLight.hollight.LT_ADD"
  "LT_0" > "HOLLight.hollight.LT_0"
  "LTE_TRANS" > "HOLLight.hollight.LTE_TRANS"
  "LTE_CASES" > "HOLLight.hollight.LTE_CASES"
  "LTE_ANTISYM" > "HOLLight.hollight.LTE_ANTISYM"
  "LTE_ADD2" > "HOLLight.hollight.LTE_ADD2"
  "LN_POW" > "HOLLight.hollight.LN_POW"
  "LN_POS_LT" > "HOLLight.hollight.LN_POS_LT"
  "LN_POS" > "HOLLight.hollight.LN_POS"
  "LN_MUL" > "HOLLight.hollight.LN_MUL"
  "LN_MONO_LT" > "HOLLight.hollight.LN_MONO_LT"
  "LN_MONO_LE" > "HOLLight.hollight.LN_MONO_LE"
  "LN_LT_X" > "HOLLight.hollight.LN_LT_X"
  "LN_LE" > "HOLLight.hollight.LN_LE"
  "LN_INV" > "HOLLight.hollight.LN_INV"
  "LN_INJ" > "HOLLight.hollight.LN_INJ"
  "LN_EXP" > "HOLLight.hollight.LN_EXP"
  "LN_DIV" > "HOLLight.hollight.LN_DIV"
  "LN_1" > "HOLLight.hollight.LN_1"
  "LIST_OF_SET_PROPERTIES" > "HOLLight.hollight.LIST_OF_SET_PROPERTIES"
  "LIM_X" > "HOLLight.hollight.LIM_X"
  "LIM_UNIQ" > "HOLLight.hollight.LIM_UNIQ"
  "LIM_TRANSFORM" > "HOLLight.hollight.LIM_TRANSFORM"
  "LIM_TENDS2" > "HOLLight.hollight.LIM_TENDS2"
  "LIM_TENDS" > "HOLLight.hollight.LIM_TENDS"
  "LIM_SUM" > "HOLLight.hollight.LIM_SUM"
  "LIM_SUB" > "HOLLight.hollight.LIM_SUB"
  "LIM_NULL" > "HOLLight.hollight.LIM_NULL"
  "LIM_NEG" > "HOLLight.hollight.LIM_NEG"
  "LIM_MUL" > "HOLLight.hollight.LIM_MUL"
  "LIM_INV" > "HOLLight.hollight.LIM_INV"
  "LIM_EQUAL" > "HOLLight.hollight.LIM_EQUAL"
  "LIM_DIV" > "HOLLight.hollight.LIM_DIV"
  "LIM_CONST" > "HOLLight.hollight.LIM_CONST"
  "LIM_ADD" > "HOLLight.hollight.LIM_ADD"
  "LIM" > "HOLLight.hollight.LIM"
  "LE_TRANS" > "HOLLight.hollight.LE_TRANS"
  "LE_SUC_LT" > "HOLLight.hollight.LE_SUC_LT"
  "LE_SUC" > "HOLLight.hollight.LE_SUC"
  "LE_SQUARE_REFL" > "HOLLight.hollight.LE_SQUARE_REFL"
  "LE_REFL" > "HOLLight.hollight.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" > "HOLLight.hollight.LE_MULT2"
  "LE_LT" > "HOLLight.hollight.LE_LT"
  "LE_LDIV_EQ" > "HOLLight.hollight.LE_LDIV_EQ"
  "LE_LDIV" > "HOLLight.hollight.LE_LDIV"
  "LE_EXP" > "HOLLight.hollight.LE_EXP"
  "LE_EXISTS" > "HOLLight.hollight.LE_EXISTS"
  "LE_CASES" > "HOLLight.hollight.LE_CASES"
  "LE_ANTISYM" > "HOLLight.hollight.LE_ANTISYM"
  "LE_ADD_RCANCEL" > "HOLLight.hollight.LE_ADD_RCANCEL"
  "LE_ADD_LCANCEL" > "HOLLight.hollight.LE_ADD_LCANCEL"
  "LE_ADDR" > "HOLLight.hollight.LE_ADDR"
  "LE_ADD2" > "HOLLight.hollight.LE_ADD2"
  "LE_ADD" > "HOLLight.hollight.LE_ADD"
  "LE_0" > "HOLLight.hollight.LE_0"
  "LET_TRANS" > "HOLLight.hollight.LET_TRANS"
  "LET_END_def" > "HOLLight.hollight.LET_END_def"
  "LET_CASES" > "HOLLight.hollight.LET_CASES"
  "LET_ANTISYM" > "HOLLight.hollight.LET_ANTISYM"
  "LET_ADD2" > "HOLLight.hollight.LET_ADD2"
  "LESS_SUC_EQ" > "HOLLight.hollight.LESS_SUC_EQ"
  "LESS_1" > "HOLLight.hollight.LESS_1"
  "LENGTH_def" > "HOLLight.hollight.LENGTH_def"
  "LENGTH_REPLICATE" > "HOLLight.hollight.LENGTH_REPLICATE"
  "LENGTH_MAP2" > "HOLLight.hollight.LENGTH_MAP2"
  "LENGTH_MAP" > "HOLLight.hollight.LENGTH_MAP"
  "LENGTH_LIST_OF_SET" > "HOLLight.hollight.LENGTH_LIST_OF_SET"
  "LENGTH_EQ_NIL" > "HOLLight.hollight.LENGTH_EQ_NIL"
  "LENGTH_EQ_CONS" > "HOLLight.hollight.LENGTH_EQ_CONS"
  "LENGTH_APPEND" > "HOLLight.hollight.LENGTH_APPEND"
  "LEFT_SUB_DISTRIB" > "Nat.nat_distrib_4"
  "LEFT_OR_FORALL_THM" > "HOL.all_simps_3"
  "LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
  "LEFT_OR_DISTRIB" > "HOL.conj_disj_distribL"
  "LEFT_IMP_FORALL_THM" > "HOL.imp_all"
  "LEFT_IMP_EXISTS_THM" > "HOL.imp_ex"
  "LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
  "LEFT_FORALL_IMP_THM" > "HOL.imp_ex"
  "LEFT_EXISTS_IMP_THM" > "HOL.imp_all"
  "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" > "Nat.nat_distrib_2"
  "LAST_def" > "HOLLight.hollight.LAST_def"
  "LAST_CLAUSES" > "HOLLight.hollight.LAST_CLAUSES"
  "LAMBDA_UNIQUE" > "HOLLight.hollight.LAMBDA_UNIQUE"
  "LAMBDA_ETA" > "HOLLight.hollight.LAMBDA_ETA"
  "LAMBDA_BETA" > "HOLLight.hollight.LAMBDA_BETA"
  "I_THM" > "Fun.id_apply"
  "I_O_ID" > "HOLLight.hollight.I_O_ID"
  "IVT_DERIVATIVE_POS" > "HOLLight.hollight.IVT_DERIVATIVE_POS"
  "IVT_DERIVATIVE_NEG" > "HOLLight.hollight.IVT_DERIVATIVE_NEG"
  "IVT_DERIVATIVE_0" > "HOLLight.hollight.IVT_DERIVATIVE_0"
  "IVT2" > "HOLLight.hollight.IVT2"
  "IVT" > "HOLLight.hollight.IVT"
  "ITSET_def" > "HOLLight.hollight.ITSET_def"
  "ITSET_EQ" > "HOLLight.hollight.ITSET_EQ"
  "ITLIST_def" > "HOLLight.hollight.ITLIST_def"
  "ITLIST_EXTRA" > "HOLLight.hollight.ITLIST_EXTRA"
  "ITLIST2_def" > "HOLLight.hollight.ITLIST2_def"
  "ITLIST2" > "HOLLight.hollight.ITLIST2"
  "ITERATE_UNION_GEN" > "HOLLight.hollight.ITERATE_UNION_GEN"
  "ITERATE_UNION" > "HOLLight.hollight.ITERATE_UNION"
  "ITERATE_SUPPORT" > "HOLLight.hollight.ITERATE_SUPPORT"
  "ITERATE_SING" > "HOLLight.hollight.ITERATE_SING"
  "ITERATE_RELATED" > "HOLLight.hollight.ITERATE_RELATED"
  "ITERATE_IMAGE" > "HOLLight.hollight.ITERATE_IMAGE"
  "ITERATE_EQ_NEUTRAL" > "HOLLight.hollight.ITERATE_EQ_NEUTRAL"
  "ITERATE_DIFF_GEN" > "HOLLight.hollight.ITERATE_DIFF_GEN"
  "ITERATE_DIFF" > "HOLLight.hollight.ITERATE_DIFF"
  "ITERATE_DELTA" > "HOLLight.hollight.ITERATE_DELTA"
  "ITERATE_CLOSED_GEN" > "HOLLight.hollight.ITERATE_CLOSED_GEN"
  "ITERATE_CLOSED" > "HOLLight.hollight.ITERATE_CLOSED"
  "ITERATE_CLAUSES_GEN" > "HOLLight.hollight.ITERATE_CLAUSES_GEN"
  "ITERATE_CLAUSES" > "HOLLight.hollight.ITERATE_CLAUSES"
  "ISO_def" > "HOLLight.hollight.ISO_def"
  "ISO_USAGE" > "HOLLight.hollight.ISO_USAGE"
  "ISO_REFL" > "HOLLight.hollight.ISO_REFL"
  "ISO_FUN" > "HOLLight.hollight.ISO_FUN"
  "ISMET_R1" > "HOLLight.hollight.ISMET_R1"
  "IN_def" > "HOLLight.hollight.IN_def"
  "IN_UNIV" > "HOLLight.hollight.IN_UNIV"
  "IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
  "IN_UNION" > "HOLLight.hollight.IN_UNION"
  "IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
  "IN_SING" > "HOLLight.hollight.IN_SING"
  "IN_SET_OF_LIST" > "HOLLight.hollight.IN_SET_OF_LIST"
  "IN_REST" > "HOLLight.hollight.IN_REST"
  "IN_NUMSEG" > "HOLLight.hollight.IN_NUMSEG"
  "IN_INTERS" > "HOLLight.hollight.IN_INTERS"
  "IN_INTER" > "HOLLight.hollight.IN_INTER"
  "IN_INSERT" > "HOLLight.hollight.IN_INSERT"
  "IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
  "IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
  "IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
  "IN_DIFF" > "HOLLight.hollight.IN_DIFF"
  "IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
  "IN_DELETE" > "HOLLight.hollight.IN_DELETE"
  "INT_POW" > "HOLLight.hollight.INT_POW"
  "INT_LT_DISCRETE" > "HOLLight.hollight.INT_LT_DISCRETE"
  "INT_LT" > "HOLLight.hollight.INT_LT"
  "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_FORALL_POS" > "HOLLight.hollight.INT_FORALL_POS"
  "INT_ARCH" > "HOLLight.hollight.INT_ARCH"
  "INT_ABS_MUL_1" > "HOLLight.hollight.INT_ABS_MUL_1"
  "INT_ABS" > "HOLLight.hollight.INT_ABS"
  "INTER_def" > "HOLLight.hollight.INTER_def"
  "INTER_UNIV" > "HOLLight.hollight.INTER_UNIV"
  "INTER_SUBSET" > "HOLLight.hollight.INTER_SUBSET"
  "INTER_OVER_UNION" > "HOLLight.hollight.INTER_OVER_UNION"
  "INTER_IDEMPOT" > "HOLLight.hollight.INTER_IDEMPOT"
  "INTER_EMPTY" > "HOLLight.hollight.INTER_EMPTY"
  "INTER_COMM" > "HOLLight.hollight.INTER_COMM"
  "INTER_ASSOC" > "HOLLight.hollight.INTER_ASSOC"
  "INTER_ACI" > "HOLLight.hollight.INTER_ACI"
  "INTERVAL_LEMMA_LT" > "HOLLight.hollight.INTERVAL_LEMMA_LT"
  "INTERVAL_LEMMA" > "HOLLight.hollight.INTERVAL_LEMMA"
  "INTERVAL_ABS" > "HOLLight.hollight.INTERVAL_ABS"
  "INTERS_def" > "HOLLight.hollight.INTERS_def"
  "INTEGRAL_NULL" > "HOLLight.hollight.INTEGRAL_NULL"
  "INSERT_def" > "HOLLight.hollight.INSERT_def"
  "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
  "INSERT_UNION_EQ" > "HOLLight.hollight.INSERT_UNION_EQ"
  "INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
  "INSERT_SUBSET" > "HOLLight.hollight.INSERT_SUBSET"
  "INSERT_INTER" > "HOLLight.hollight.INSERT_INTER"
  "INSERT_INSERT" > "HOLLight.hollight.INSERT_INSERT"
  "INSERT_DIFF" > "HOLLight.hollight.INSERT_DIFF"
  "INSERT_DELETE" > "HOLLight.hollight.INSERT_DELETE"
  "INSERT_COMM" > "HOLLight.hollight.INSERT_COMM"
  "INSERT_AC" > "HOLLight.hollight.INSERT_AC"
  "INSERT" > "HOLLight.hollight.INSERT"
  "INR_def" > "HOLLight.hollight.INR_def"
  "INL_def" > "HOLLight.hollight.INL_def"
  "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_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_LEFT_INVERSE"
  "INJA_def" > "HOLLight.hollight.INJA_def"
  "INJA_INJ" > "HOLLight.hollight.INJA_INJ"
  "INFINITE_def" > "HOLLight.hollight.INFINITE_def"
  "INFINITE_NONEMPTY" > "HOLLight.hollight.INFINITE_NONEMPTY"
  "INFINITE_IMAGE_INJ" > "HOLLight.hollight.INFINITE_IMAGE_INJ"
  "INFINITE_DIFF_FINITE" > "HOLLight.hollight.INFINITE_DIFF_FINITE"
  "IMP_EQ_CLAUSE" > "HOLLight.hollight.IMP_EQ_CLAUSE"
  "IMP_CONJ" > "HOL.imp_conjL"
  "IMP_CLAUSES" > "HOLLight.hollight.IMP_CLAUSES"
  "IMAGE_o" > "HOLLight.hollight.IMAGE_o"
  "IMAGE_def" > "HOLLight.hollight.IMAGE_def"
  "IMAGE_UNION" > "HOLLight.hollight.IMAGE_UNION"
  "IMAGE_SUBSET" > "HOLLight.hollight.IMAGE_SUBSET"
  "IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
  "IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
  "IMAGE_EQ_EMPTY" > "HOLLight.hollight.IMAGE_EQ_EMPTY"
  "IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
  "IMAGE_DELETE_INJ" > "HOLLight.hollight.IMAGE_DELETE_INJ"
  "IMAGE_CONST" > "HOLLight.hollight.IMAGE_CONST"
  "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_def" > "HOLLight.hollight.HD_def"
  "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" > "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_CLAUSES" > "HOLLight.hollight.HAS_SIZE_CLAUSES"
  "HAS_SIZE_CARD" > "HOLLight.hollight.HAS_SIZE_CARD"
  "HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
  "GSPEC_def" > "HOLLight.hollight.GSPEC_def"
  "GP_FINITE" > "HOLLight.hollight.GP_FINITE"
  "GP" > "HOLLight.hollight.GP"
  "GEQ_def" > "HOLLight.hollight.GEQ_def"
  "GAUGE_MIN" > "HOLLight.hollight.GAUGE_MIN"
  "GABS_def" > "HOLLight.hollight.GABS_def"
  "FUN_EQ_THM" > "Fun.expand_fun_eq"
  "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
  "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
  "FTC1" > "HOLLight.hollight.FTC1"
  "FSTCART_PASTECART" > "HOLLight.hollight.FSTCART_PASTECART"
  "FST" > "Product_Type.fst_conv"
  "FORALL_SIMP" > "HOL.simp_thms_35"
  "FORALL_PASTECART" > "HOLLight.hollight.FORALL_PASTECART"
  "FORALL_PAIR_THM" > "Product_Type.split_paired_All"
  "FORALL_NOT_THM" > "Inductive.basic_monos_16"
  "FORALL_IN_UNIONS" > "HOLLight.hollight.FORALL_IN_UNIONS"
  "FORALL_IN_IMAGE" > "HOLLight.hollight.FORALL_IN_IMAGE"
  "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" > "HOLLight.hollight.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_def" > "HOLLight.hollight.FINITE_def"
  "FINITE_UNION_IMP" > "HOLLight.hollight.FINITE_UNION_IMP"
  "FINITE_UNIONS" > "HOLLight.hollight.FINITE_UNIONS"
  "FINITE_UNION" > "HOLLight.hollight.FINITE_UNION"
  "FINITE_SUPPORT_DELTA" > "HOLLight.hollight.FINITE_SUPPORT_DELTA"
  "FINITE_SUPPORT" > "HOLLight.hollight.FINITE_SUPPORT"
  "FINITE_SUBSET_IMAGE_IMP" > "HOLLight.hollight.FINITE_SUBSET_IMAGE_IMP"
  "FINITE_SUBSET_IMAGE" > "HOLLight.hollight.FINITE_SUBSET_IMAGE"
  "FINITE_SUBSETS" > "HOLLight.hollight.FINITE_SUBSETS"
  "FINITE_SUBSET" > "HOLLight.hollight.FINITE_SUBSET"
  "FINITE_SET_OF_LIST" > "HOLLight.hollight.FINITE_SET_OF_LIST"
  "FINITE_RESTRICT" > "HOLLight.hollight.FINITE_RESTRICT"
  "FINITE_RECURSION_DELETE" > "HOLLight.hollight.FINITE_RECURSION_DELETE"
  "FINITE_RECURSION" > "HOLLight.hollight.FINITE_RECURSION"
  "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" > "HOLLight.hollight.FINITE_NUMSEG"
  "FINITE_INTER" > "HOLLight.hollight.FINITE_INTER"
  "FINITE_INSERT" > "HOLLight.hollight.FINITE_INSERT"
  "FINITE_INDUCT_STRONG" > "HOLLight.hollight.FINITE_INDUCT_STRONG"
  "FINITE_INDEX_WORKS_FINITE" > "HOLLight.hollight.FINITE_INDEX_WORKS_FINITE"
  "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_INJ" > "HOLLight.hollight.FINITE_INDEX_INJ"
  "FINITE_IMAGE_INJ_GENERAL" > "HOLLight.hollight.FINITE_IMAGE_INJ_GENERAL"
  "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" > "HOLLight.hollight.FINITE_IMAGE"
  "FINITE_HAS_SIZE_LEMMA" > "HOLLight.hollight.FINITE_HAS_SIZE_LEMMA"
  "FINITE_FUNSPACE" > "HOLLight.hollight.FINITE_FUNSPACE"
  "FINITE_FINITE_IMAGE" > "HOLLight.hollight.FINITE_FINITE_IMAGE"
  "FINITE_DIFF" > "HOLLight.hollight.FINITE_DIFF"
  "FINITE_DELETE_IMP" > "HOLLight.hollight.FINITE_DELETE_IMP"
  "FINITE_DELETE" > "HOLLight.hollight.FINITE_DELETE"
  "FINE_MIN" > "HOLLight.hollight.FINE_MIN"
  "FILTER_def" > "HOLLight.hollight.FILTER_def"
  "FILTER_MAP" > "HOLLight.hollight.FILTER_MAP"
  "FILTER_APPEND" > "HOLLight.hollight.FILTER_APPEND"
  "FCONS_def" > "HOLLight.hollight.FCONS_def"
  "FCONS_UNDO" > "HOLLight.hollight.FCONS_UNDO"
  "FACT_def" > "HOLLight.hollight.FACT_def"
  "FACT_MONO" > "HOLLight.hollight.FACT_MONO"
  "FACT_LT" > "HOLLight.hollight.FACT_LT"
  "FACT_LE" > "HOLLight.hollight.FACT_LE"
  "EX_def" > "HOLLight.hollight.EX_def"
  "EX_MEM" > "HOLLight.hollight.EX_MEM"
  "EX_MAP" > "HOLLight.hollight.EX_MAP"
  "EX_IMP" > "HOLLight.hollight.EX_IMP"
  "EXTENSION" > "HOLLight.hollight.EXTENSION"
  "EXP_def" > "HOLLight.hollight.EXP_def"
  "EXP_ONE" > "HOLLight.hollight.EXP_ONE"
  "EXP_MULT" > "HOLLight.hollight.EXP_MULT"
  "EXP_LT_0" > "HOLLight.hollight.EXP_LT_0"
  "EXP_EQ_0" > "HOLLight.hollight.EXP_EQ_0"
  "EXP_ADD" > "HOLLight.hollight.EXP_ADD"
  "EXP_2" > "HOLLight.hollight.EXP_2"
  "EXP_1" > "HOLLight.hollight.EXP_1"
  "EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF"
  "EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
  "EXISTS_UNIQUE_ALT" > "HOLLight.hollight.EXISTS_UNIQUE_ALT"
  "EXISTS_UNIQUE" > "HOL.Ex1_def"
  "EXISTS_THM" > "HOL4Setup.EXISTS_DEF"
  "EXISTS_SIMP" > "HOL.simp_thms_36"
  "EXISTS_REFL" > "HOL.simp_thms_37"
  "EXISTS_PASTECART" > "HOLLight.hollight.EXISTS_PASTECART"
  "EXISTS_PAIR_THM" > "Product_Type.split_paired_Ex"
  "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
  "EXISTS_ONE_REP" > "HOLLight.hollight.EXISTS_ONE_REP"
  "EXISTS_NOT_THM" > "Inductive.basic_monos_15"
  "EXISTS_IN_IMAGE" > "HOLLight.hollight.EXISTS_IN_IMAGE"
  "EXISTS_IN_CLAUSES" > "HOLLight.hollight.EXISTS_IN_CLAUSES"
  "EXISTS_EX" > "HOLLight.hollight.EXISTS_EX"
  "EXISTS_BOOL_THM" > "Set.ex_bool_eq"
  "EXCLUDED_MIDDLE" > "HOLLight.hollight.EXCLUDED_MIDDLE"
  "EVEN_def" > "HOLLight.hollight.EVEN_def"
  "EVEN_OR_ODD" > "HOLLight.hollight.EVEN_OR_ODD"
  "EVEN_ODD_DECOMPOSITION" > "HOLLight.hollight.EVEN_ODD_DECOMPOSITION"
  "EVEN_MULT" > "HOLLight.hollight.EVEN_MULT"
  "EVEN_MOD" > "HOLLight.hollight.EVEN_MOD"
  "EVEN_EXP" > "HOLLight.hollight.EVEN_EXP"
  "EVEN_EXISTS_LEMMA" > "HOLLight.hollight.EVEN_EXISTS_LEMMA"
  "EVEN_EXISTS" > "HOLLight.hollight.EVEN_EXISTS"
  "EVEN_DOUBLE" > "HOLLight.hollight.EVEN_DOUBLE"
  "EVEN_DIV2" > "HOLLight.hollight.EVEN_DIV2"
  "EVEN_AND_ODD" > "HOLLight.hollight.EVEN_AND_ODD"
  "EVEN_ADD" > "HOLLight.hollight.EVEN_ADD"
  "EQ_UNIV" > "HOLLight.hollight.EQ_UNIV"
  "EQ_TRANS" > "Set.basic_trans_rules_31"
  "EQ_SYM_EQ" > "HOL.eq_sym_conv"
  "EQ_SYM" > "HOL.meta_eq_to_obj_eq"
  "EQ_SUC" > "Nat.nat.simps_3"
  "EQ_REFL_T" > "HOL.simp_thms_6"
  "EQ_REFL" > "Presburger.fm_modd_pinf"
  "EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
  "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
  "EQ_IMP_LE" > "HOLLight.hollight.EQ_IMP_LE"
  "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
  "EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
  "EQ_ADD_RCANCEL_0" > "HOLLight.hollight.EQ_ADD_RCANCEL_0"
  "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
  "EQ_ADD_LCANCEL_0" > "HOLLight.hollight.EQ_ADD_LCANCEL_0"
  "EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel"
  "EMPTY_def" > "HOLLight.hollight.EMPTY_def"
  "EMPTY_UNIONS" > "HOLLight.hollight.EMPTY_UNIONS"
  "EMPTY_UNION" > "HOLLight.hollight.EMPTY_UNION"
  "EMPTY_SUBSET" > "HOLLight.hollight.EMPTY_SUBSET"
  "EMPTY_NOT_UNIV" > "HOLLight.hollight.EMPTY_NOT_UNIV"
  "EMPTY_GSPEC" > "HOLLight.hollight.EMPTY_GSPEC"
  "EMPTY_DIFF" > "HOLLight.hollight.EMPTY_DIFF"
  "EMPTY_DELETE" > "HOLLight.hollight.EMPTY_DELETE"
  "EL_def" > "HOLLight.hollight.EL_def"
  "DORDER_TENDSTO" > "HOLLight.hollight.DORDER_TENDSTO"
  "DORDER_NGE" > "HOLLight.hollight.DORDER_NGE"
  "DORDER_LEMMA" > "HOLLight.hollight.DORDER_LEMMA"
  "DIV_def" > "HOLLight.hollight.DIV_def"
  "DIV_UNIQ" > "HOLLight.hollight.DIV_UNIQ"
  "DIV_REFL" > "HOLLight.hollight.DIV_REFL"
  "DIV_MUL_LE" > "HOLLight.hollight.DIV_MUL_LE"
  "DIV_MULT2" > "HOLLight.hollight.DIV_MULT2"
  "DIV_MULT" > "HOLLight.hollight.DIV_MULT"
  "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" > "HOLLight.hollight.DIV_LT"
  "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"
  "DIV_1" > "HOLLight.hollight.DIV_1"
  "DIV_0" > "HOLLight.hollight.DIV_0"
  "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_UBOUND_LT" > "HOLLight.hollight.DIVISION_UBOUND_LT"
  "DIVISION_UBOUND" > "HOLLight.hollight.DIVISION_UBOUND"
  "DIVISION_THM" > "HOLLight.hollight.DIVISION_THM"
  "DIVISION_SINGLE" > "HOLLight.hollight.DIVISION_SINGLE"
  "DIVISION_RHS" > "HOLLight.hollight.DIVISION_RHS"
  "DIVISION_LT_GEN" > "HOLLight.hollight.DIVISION_LT_GEN"
  "DIVISION_LT" > "HOLLight.hollight.DIVISION_LT"
  "DIVISION_LHS" > "HOLLight.hollight.DIVISION_LHS"
  "DIVISION_LE" > "HOLLight.hollight.DIVISION_LE"
  "DIVISION_LBOUND_LT" > "HOLLight.hollight.DIVISION_LBOUND_LT"
  "DIVISION_LBOUND" > "HOLLight.hollight.DIVISION_LBOUND"
  "DIVISION_GT" > "HOLLight.hollight.DIVISION_GT"
  "DIVISION_EXISTS" > "HOLLight.hollight.DIVISION_EXISTS"
  "DIVISION_EQ" > "HOLLight.hollight.DIVISION_EQ"
  "DIVISION_APPEND_LEMMA2" > "HOLLight.hollight.DIVISION_APPEND_LEMMA2"
  "DIVISION_APPEND_LEMMA1" > "HOLLight.hollight.DIVISION_APPEND_LEMMA1"
  "DIVISION_APPEND" > "HOLLight.hollight.DIVISION_APPEND"
  "DIVISION_1" > "HOLLight.hollight.DIVISION_1"
  "DIVISION_0" > "HOLLight.hollight.DIVISION_0"
  "DIVISION" > "HOLLight.hollight.DIVISION"
  "DIST_TRIANGLE_LE" > "HOLLight.hollight.DIST_TRIANGLE_LE"
  "DIST_TRIANGLES_LE" > "HOLLight.hollight.DIST_TRIANGLES_LE"
  "DIST_TRIANGLE" > "HOLLight.hollight.DIST_TRIANGLE"
  "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"
  "DIST_ADDBOUND" > "HOLLight.hollight.DIST_ADDBOUND"
  "DIST_ADD2_REV" > "HOLLight.hollight.DIST_ADD2_REV"
  "DIST_ADD2" > "HOLLight.hollight.DIST_ADD2"
  "DISJ_SYM" > "HOL.disj_comms_1"
  "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
  "DISJ_ACI" > "HOLLight.hollight.DISJ_ACI"
  "DISJOINT_def" > "HOLLight.hollight.DISJOINT_def"
  "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"
  "DINT_UNIQ" > "HOLLight.hollight.DINT_UNIQ"
  "DIMINDEX_NONZERO" > "HOLLight.hollight.DIMINDEX_NONZERO"
  "DIMINDEX_HAS_SIZE_FINITE_SUM" > "HOLLight.hollight.DIMINDEX_HAS_SIZE_FINITE_SUM"
  "DIMINDEX_GE_1" > "HOLLight.hollight.DIMINDEX_GE_1"
  "DIMINDEX_FINITE_SUM" > "HOLLight.hollight.DIMINDEX_FINITE_SUM"
  "DIMINDEX_FINITE_IMAGE" > "HOLLight.hollight.DIMINDEX_FINITE_IMAGE"
  "DIFF_def" > "HOLLight.hollight.DIFF_def"
  "DIFF_XM1" > "HOLLight.hollight.DIFF_XM1"
  "DIFF_X" > "HOLLight.hollight.DIFF_X"
  "DIFF_UNIV" > "HOLLight.hollight.DIFF_UNIV"
  "DIFF_UNIQ" > "HOLLight.hollight.DIFF_UNIQ"
  "DIFF_TAN_COMPOSITE" > "HOLLight.hollight.DIFF_TAN_COMPOSITE"
  "DIFF_TAN" > "HOLLight.hollight.DIFF_TAN"
  "DIFF_SUM" > "HOLLight.hollight.DIFF_SUM"
  "DIFF_SUB" > "HOLLight.hollight.DIFF_SUB"
  "DIFF_SIN" > "HOLLight.hollight.DIFF_SIN"
  "DIFF_POW" > "HOLLight.hollight.DIFF_POW"
  "DIFF_NEG" > "HOLLight.hollight.DIFF_NEG"
  "DIFF_MUL" > "HOLLight.hollight.DIFF_MUL"
  "DIFF_LN_COMPOSITE" > "HOLLight.hollight.DIFF_LN_COMPOSITE"
  "DIFF_LN" > "HOLLight.hollight.DIFF_LN"
  "DIFF_LMIN" > "HOLLight.hollight.DIFF_LMIN"
  "DIFF_LMAX" > "HOLLight.hollight.DIFF_LMAX"
  "DIFF_LINC" > "HOLLight.hollight.DIFF_LINC"
  "DIFF_LDEC" > "HOLLight.hollight.DIFF_LDEC"
  "DIFF_LCONST" > "HOLLight.hollight.DIFF_LCONST"
  "DIFF_ISCONST_END_SIMPLE" > "HOLLight.hollight.DIFF_ISCONST_END_SIMPLE"
  "DIFF_ISCONST_END" > "HOLLight.hollight.DIFF_ISCONST_END"
  "DIFF_ISCONST_ALL" > "HOLLight.hollight.DIFF_ISCONST_ALL"
  "DIFF_ISCONST" > "HOLLight.hollight.DIFF_ISCONST"
  "DIFF_INVERSE_LT" > "HOLLight.hollight.DIFF_INVERSE_LT"
  "DIFF_INVERSE" > "HOLLight.hollight.DIFF_INVERSE"
  "DIFF_INV" > "HOLLight.hollight.DIFF_INV"
  "DIFF_INSERT" > "HOLLight.hollight.DIFF_INSERT"
  "DIFF_EXP" > "HOLLight.hollight.DIFF_EXP"
  "DIFF_EQ_EMPTY" > "HOLLight.hollight.DIFF_EQ_EMPTY"
  "DIFF_EMPTY" > "HOLLight.hollight.DIFF_EMPTY"
  "DIFF_DIV" > "HOLLight.hollight.DIFF_DIV"
  "DIFF_DIFF" > "HOLLight.hollight.DIFF_DIFF"
  "DIFF_COS" > "HOLLight.hollight.DIFF_COS"
  "DIFF_CONT" > "HOLLight.hollight.DIFF_CONT"
  "DIFF_CONST" > "HOLLight.hollight.DIFF_CONST"
  "DIFF_COMPOSITE" > "HOLLight.hollight.DIFF_COMPOSITE"
  "DIFF_CMUL" > "HOLLight.hollight.DIFF_CMUL"
  "DIFF_CHAIN" > "HOLLight.hollight.DIFF_CHAIN"
  "DIFF_CARAT" > "HOLLight.hollight.DIFF_CARAT"
  "DIFF_ATN_COMPOSITE" > "HOLLight.hollight.DIFF_ATN_COMPOSITE"
  "DIFF_ATN" > "HOLLight.hollight.DIFF_ATN"
  "DIFF_ASN_COS" > "HOLLight.hollight.DIFF_ASN_COS"
  "DIFF_ASN" > "HOLLight.hollight.DIFF_ASN"
  "DIFF_ADD" > "HOLLight.hollight.DIFF_ADD"
  "DIFF_ACS_SIN" > "HOLLight.hollight.DIFF_ACS_SIN"
  "DIFF_ACS" > "HOLLight.hollight.DIFF_ACS"
  "DIFFS_NEG" > "HOLLight.hollight.DIFFS_NEG"
  "DIFFS_LEMMA2" > "HOLLight.hollight.DIFFS_LEMMA2"
  "DIFFS_LEMMA" > "HOLLight.hollight.DIFFS_LEMMA"
  "DIFFS_EQUIV" > "HOLLight.hollight.DIFFS_EQUIV"
  "DEST_REC_INJ" > "HOLLight.hollight.recspace._dest_rec_inject"
  "DELETE_def" > "HOLLight.hollight.DELETE_def"
  "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_~" > "HOL.simp_thms_19"
  "DEF_two_2" > "HOLLight.hollight.DEF_two_2"
  "DEF_two_1" > "HOLLight.hollight.DEF_two_1"
  "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_three_3" > "HOLLight.hollight.DEF_three_3"
  "DEF_three_2" > "HOLLight.hollight.DEF_three_2"
  "DEF_three_1" > "HOLLight.hollight.DEF_three_1"
  "DEF_tendsto" > "HOLLight.hollight.DEF_tendsto"
  "DEF_tends_real_real" > "HOLLight.hollight.DEF_tends_real_real"
  "DEF_tends_num_real" > "HOLLight.hollight.DEF_tends_num_real"
  "DEF_tends" > "HOLLight.hollight.DEF_tends"
  "DEF_tdiv" > "HOLLight.hollight.DEF_tdiv"
  "DEF_tan" > "HOLLight.hollight.DEF_tan"
  "DEF_tailadmissible" > "HOLLight.hollight.DEF_tailadmissible"
  "DEF_support" > "HOLLight.hollight.DEF_support"
  "DEF_superadmissible" > "HOLLight.hollight.DEF_superadmissible"
  "DEF_sup" > "HOLLight.hollight.DEF_sup"
  "DEF_sums" > "HOLLight.hollight.DEF_sums"
  "DEF_summable" > "HOLLight.hollight.DEF_summable"
  "DEF_suminf" > "HOLLight.hollight.DEF_suminf"
  "DEF_sum" > "HOLLight.hollight.DEF_sum"
  "DEF_subseq" > "HOLLight.hollight.DEF_subseq"
  "DEF_sqrt" > "HOLLight.hollight.DEF_sqrt"
  "DEF_sndcart" > "HOLLight.hollight.DEF_sndcart"
  "DEF_sin" > "HOLLight.hollight.DEF_sin"
  "DEF_set_of_list" > "HOLLight.hollight.DEF_set_of_list"
  "DEF_rsum" > "HOLLight.hollight.DEF_rsum"
  "DEF_root" > "HOLLight.hollight.DEF_root"
  "DEF_real_sub" > "HOLLight.hollight.DEF_real_sub"
  "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_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_re_universe" > "HOLLight.hollight.DEF_re_universe"
  "DEF_re_union" > "HOLLight.hollight.DEF_re_union"
  "DEF_re_subset" > "HOLLight.hollight.DEF_re_subset"
  "DEF_re_null" > "HOLLight.hollight.DEF_re_null"
  "DEF_re_intersect" > "HOLLight.hollight.DEF_re_intersect"
  "DEF_re_compl" > "HOLLight.hollight.DEF_re_compl"
  "DEF_re_Union" > "HOLLight.hollight.DEF_re_Union"
  "DEF_psum" > "HOLLight.hollight.DEF_psum"
  "DEF_pi" > "HOLLight.hollight.DEF_pi"
  "DEF_pastecart" > "HOLLight.hollight.DEF_pastecart"
  "DEF_pairwise" > "HOLLight.hollight.DEF_pairwise"
  "DEF_o" > "Fun.o_apply"
  "DEF_nsum" > "HOLLight.hollight.DEF_nsum"
  "DEF_neutral" > "HOLLight.hollight.DEF_neutral"
  "DEF_neigh" > "HOLLight.hollight.DEF_neigh"
  "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_mtop" > "HOLLight.hollight.DEF_mtop"
  "DEF_mr1" > "HOLLight.hollight.DEF_mr1"
  "DEF_monoidal" > "HOLLight.hollight.DEF_monoidal"
  "DEF_mono" > "HOLLight.hollight.DEF_mono"
  "DEF_mod_real" > "HOLLight.hollight.DEF_mod_real"
  "DEF_mod_nat" > "HOLLight.hollight.DEF_mod_nat"
  "DEF_mod_int" > "HOLLight.hollight.DEF_mod_int"
  "DEF_mk_pair" > "Product_Type.Pair_Rep_def"
  "DEF_minimal" > "HOLLight.hollight.DEF_minimal"
  "DEF_measure" > "HOLLight.hollight.DEF_measure"
  "DEF_ln" > "HOLLight.hollight.DEF_ln"
  "DEF_list_of_set" > "HOLLight.hollight.DEF_list_of_set"
  "DEF_limpt" > "HOLLight.hollight.DEF_limpt"
  "DEF_lim" > "HOLLight.hollight.DEF_lim"
  "DEF_lambda" > "HOLLight.hollight.DEF_lambda"
  "DEF_iterate" > "HOLLight.hollight.DEF_iterate"
  "DEF_istopology" > "HOLLight.hollight.DEF_istopology"
  "DEF_ismet" > "HOLLight.hollight.DEF_ismet"
  "DEF_is_nadd" > "HOLLight.hollight.DEF_is_nadd"
  "DEF_is_int" > "HOLLight.hollight.DEF_is_int"
  "DEF_int_sub" > "HOLLight.hollight.DEF_int_sub"
  "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_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_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_gauge" > "HOLLight.hollight.DEF_gauge"
  "DEF_fstcart" > "HOLLight.hollight.DEF_fstcart"
  "DEF_finite_index" > "HOLLight.hollight.DEF_finite_index"
  "DEF_fine" > "HOLLight.hollight.DEF_fine"
  "DEF_exp" > "HOLLight.hollight.DEF_exp"
  "DEF_dsize" > "HOLLight.hollight.DEF_dsize"
  "DEF_dorder" > "HOLLight.hollight.DEF_dorder"
  "DEF_division" > "HOLLight.hollight.DEF_division"
  "DEF_dist" > "HOLLight.hollight.DEF_dist"
  "DEF_dimindex" > "HOLLight.hollight.DEF_dimindex"
  "DEF_diffs" > "HOLLight.hollight.DEF_diffs"
  "DEF_diffl" > "HOLLight.hollight.DEF_diffl"
  "DEF_differentiable" > "HOLLight.hollight.DEF_differentiable"
  "DEF_defint" > "HOLLight.hollight.DEF_defint"
  "DEF_cos" > "HOLLight.hollight.DEF_cos"
  "DEF_convergent" > "HOLLight.hollight.DEF_convergent"
  "DEF_contl" > "HOLLight.hollight.DEF_contl"
  "DEF_closed" > "HOLLight.hollight.DEF_closed"
  "DEF_cauchy" > "HOLLight.hollight.DEF_cauchy"
  "DEF_bounded" > "HOLLight.hollight.DEF_bounded"
  "DEF_ball" > "HOLLight.hollight.DEF_ball"
  "DEF_atn" > "HOLLight.hollight.DEF_atn"
  "DEF_asn" > "HOLLight.hollight.DEF_asn"
  "DEF_admissible" > "HOLLight.hollight.DEF_admissible"
  "DEF_acs" > "HOLLight.hollight.DEF_acs"
  "DEF__star_" > "HOLLightCompat.mult_altdef"
  "DEF__slash__backslash_" > "HOLLightCompat.light_and_def"
  "DEF__questionmark__exclamationmark_" > "HOL4Compat.EXISTS_UNIQUE_DEF"
  "DEF__questionmark_" > "HOL.Ex_def"
  "DEF__lessthan__equal_" > "HOLLight.hollight.DEF__lessthan__equal_"
  "DEF__lessthan_" > "HOLLight.hollight.DEF__lessthan_"
  "DEF__greaterthan__equal_" > "HOLLight.hollight.DEF__greaterthan__equal_"
  "DEF__greaterthan_" > "HOLLight.hollight.DEF__greaterthan_"
  "DEF__exclamationmark_" > "HOL.All_def"
  "DEF__equal__equal__greaterthan_" > "HOLLightCompat.light_imp_def"
  "DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
  "DEF__dot__dot_" > "HOLLight.hollight.DEF__dot__dot_"
  "DEF__backslash__slash_" > "HOL.or_def"
  "DEF__FALSITY_" > "HOLLight.hollight.DEF__FALSITY_"
  "DEF__10314" > "HOLLight.hollight.DEF__10314"
  "DEF__10313" > "HOLLight.hollight.DEF__10313"
  "DEF__10312" > "HOLLight.hollight.DEF__10312"
  "DEF__10289" > "HOLLight.hollight.DEF__10289"
  "DEF__10288" > "HOLLight.hollight.DEF__10288"
  "DEF_ZRECSPACE" > "HOLLight.hollight.DEF_ZRECSPACE"
  "DEF_ZIP" > "HOLLight.hollight.DEF_ZIP"
  "DEF_ZCONSTR" > "HOLLight.hollight.DEF_ZCONSTR"
  "DEF_ZBOT" > "HOLLight.hollight.DEF_ZBOT"
  "DEF_WF" > "HOLLight.hollight.DEF_WF"
  "DEF_UNIV" > "HOLLight.hollight.DEF_UNIV"
  "DEF_UNIONS" > "HOLLight.hollight.DEF_UNIONS"
  "DEF_UNION" > "HOLLight.hollight.DEF_UNION"
  "DEF_UNCURRY" > "HOLLight.hollight.DEF_UNCURRY"
  "DEF_TL" > "HOLLight.hollight.DEF_TL"
  "DEF_T" > "HOL.True_def"
  "DEF_SURJ" > "HOLLight.hollight.DEF_SURJ"
  "DEF_SUBSET" > "HOLLight.hollight.DEF_SUBSET"
  "DEF_SOME" > "HOLLight.hollight.DEF_SOME"
  "DEF_SND" > "HOLLightCompat.snd_altdef"
  "DEF_SING" > "HOLLight.hollight.DEF_SING"
  "DEF_SETSPEC" > "HOLLight.hollight.DEF_SETSPEC"
  "DEF_REVERSE" > "HOLLight.hollight.DEF_REVERSE"
  "DEF_REST" > "HOLLight.hollight.DEF_REST"
  "DEF_REPLICATE" > "HOLLight.hollight.DEF_REPLICATE"
  "DEF_PSUBSET" > "HOLLight.hollight.DEF_PSUBSET"
  "DEF_PRE" > "HOLLightCompat.Pred_altdef"
  "DEF_PASSOC" > "HOLLight.hollight.DEF_PASSOC"
  "DEF_PAIRWISE" > "HOLLight.hollight.DEF_PAIRWISE"
  "DEF_OUTR" > "HOLLight.hollight.DEF_OUTR"
  "DEF_OUTL" > "HOLLight.hollight.DEF_OUTL"
  "DEF_ONTO" > "Fun.surj_def"
  "DEF_ONE_ONE" > "HOL4Setup.ONE_ONE_DEF"
  "DEF_ODD" > "HOLLight.hollight.DEF_ODD"
  "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_rew"
  "DEF_NULL" > "HOLLight.hollight.DEF_NULL"
  "DEF_NONE" > "HOLLight.hollight.DEF_NONE"
  "DEF_NIL" > "HOLLight.hollight.DEF_NIL"
  "DEF_MOD" > "HOLLight.hollight.DEF_MOD"
  "DEF_MEM" > "HOLLight.hollight.DEF_MEM"
  "DEF_MAP2" > "HOLLight.hollight.DEF_MAP2"
  "DEF_MAP" > "HOLLight.hollight.DEF_MAP"
  "DEF_LET_END" > "HOLLight.hollight.DEF_LET_END"
  "DEF_LET" > "HOL4Compat.LET_def"
  "DEF_LENGTH" > "HOLLight.hollight.DEF_LENGTH"
  "DEF_LAST" > "HOLLight.hollight.DEF_LAST"
  "DEF_ITSET" > "HOLLight.hollight.DEF_ITSET"
  "DEF_ITLIST2" > "HOLLight.hollight.DEF_ITLIST2"
  "DEF_ITLIST" > "HOLLight.hollight.DEF_ITLIST"
  "DEF_ISO" > "HOLLight.hollight.DEF_ISO"
  "DEF_INTERS" > "HOLLight.hollight.DEF_INTERS"
  "DEF_INTER" > "HOLLight.hollight.DEF_INTER"
  "DEF_INSERT" > "HOLLight.hollight.DEF_INSERT"
  "DEF_INR" > "HOLLight.hollight.DEF_INR"
  "DEF_INL" > "HOLLight.hollight.DEF_INL"
  "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" > "HOLLight.hollight.DEF_INFINITE"
  "DEF_IN" > "HOLLight.hollight.DEF_IN"
  "DEF_IMAGE" > "HOLLight.hollight.DEF_IMAGE"
  "DEF_I" > "Fun.id_apply"
  "DEF_HD" > "HOLLight.hollight.DEF_HD"
  "DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
  "DEF_GSPEC" > "HOLLight.hollight.DEF_GSPEC"
  "DEF_GEQ" > "HOLLight.hollight.DEF_GEQ"
  "DEF_GABS" > "HOLLight.hollight.DEF_GABS"
  "DEF_FST" > "HOLLightCompat.fst_altdef"
  "DEF_FNIL" > "HOLLight.hollight.DEF_FNIL"
  "DEF_FINREC" > "HOLLight.hollight.DEF_FINREC"
  "DEF_FINITE" > "HOLLight.hollight.DEF_FINITE"
  "DEF_FILTER" > "HOLLight.hollight.DEF_FILTER"
  "DEF_FCONS" > "HOLLight.hollight.DEF_FCONS"
  "DEF_FACT" > "HOLLight.hollight.DEF_FACT"
  "DEF_F" > "HOL.False_def"
  "DEF_EXP" > "HOLLight.hollight.DEF_EXP"
  "DEF_EX" > "HOLLight.hollight.DEF_EX"
  "DEF_EVEN" > "HOLLight.hollight.DEF_EVEN"
  "DEF_EMPTY" > "HOLLight.hollight.DEF_EMPTY"
  "DEF_EL" > "HOLLight.hollight.DEF_EL"
  "DEF_DIV" > "HOLLight.hollight.DEF_DIV"
  "DEF_DISJOINT" > "HOLLight.hollight.DEF_DISJOINT"
  "DEF_DIFF" > "HOLLight.hollight.DEF_DIFF"
  "DEF_DELETE" > "HOLLight.hollight.DEF_DELETE"
  "DEF_DECIMAL" > "HOLLight.hollight.DEF_DECIMAL"
  "DEF_CURRY" > "HOLLight.hollight.DEF_CURRY"
  "DEF_COUNTABLE" > "HOLLight.hollight.DEF_COUNTABLE"
  "DEF_CONSTR" > "HOLLight.hollight.DEF_CONSTR"
  "DEF_CONS" > "HOLLight.hollight.DEF_CONS"
  "DEF_COND" > "HOLLight.hollight.DEF_COND"
  "DEF_CHOICE" > "HOLLight.hollight.DEF_CHOICE"
  "DEF_CASEWISE" > "HOLLight.hollight.DEF_CASEWISE"
  "DEF_CARD_LT" > "HOLLight.hollight.DEF_CARD_LT"
  "DEF_CARD_LE" > "HOLLight.hollight.DEF_CARD_LE"
  "DEF_CARD_GT" > "HOLLight.hollight.DEF_CARD_GT"
  "DEF_CARD_GE" > "HOLLight.hollight.DEF_CARD_GE"
  "DEF_CARD_EQ" > "HOLLight.hollight.DEF_CARD_EQ"
  "DEF_CARD" > "HOLLight.hollight.DEF_CARD"
  "DEF_BOTTOM" > "HOLLight.hollight.DEF_BOTTOM"
  "DEF_BIT1" > "HOLLightCompat.NUMERAL_BIT1_altdef"
  "DEF_BIT0" > "HOLLightCompat.NUMERAL_BIT0_def"
  "DEF_BIJ" > "HOLLight.hollight.DEF_BIJ"
  "DEF_ASSOC" > "HOLLight.hollight.DEF_ASSOC"
  "DEF_APPEND" > "HOLLight.hollight.DEF_APPEND"
  "DEF_ALL2" > "HOLLight.hollight.DEF_ALL2"
  "DEF_ALL" > "HOLLight.hollight.DEF_ALL"
  "DEF_-" > "HOLLightCompat.sub_altdef"
  "DEF_," > "Product_Type.Pair_def"
  "DEF_+" > "HOLLightCompat.add_altdef"
  "DEF_$" > "HOLLight.hollight.DEF_$"
  "DECOMPOSITION" > "HOLLight.hollight.DECOMPOSITION"
  "DECIMAL_def" > "HOLLight.hollight.DECIMAL_def"
  "CURRY_def" > "HOLLight.hollight.CURRY_def"
  "COUNTABLE_def" > "HOLLight.hollight.COUNTABLE_def"
  "COS_ZERO_LEMMA" > "HOLLight.hollight.COS_ZERO_LEMMA"
  "COS_ZERO" > "HOLLight.hollight.COS_ZERO"
  "COS_TOTAL" > "HOLLight.hollight.COS_TOTAL"
  "COS_SIN_SQRT" > "HOLLight.hollight.COS_SIN_SQRT"
  "COS_SIN" > "HOLLight.hollight.COS_SIN"
  "COS_POS_PI2" > "HOLLight.hollight.COS_POS_PI2"
  "COS_POS_PI" > "HOLLight.hollight.COS_POS_PI"
  "COS_PI2" > "HOLLight.hollight.COS_PI2"
  "COS_PI" > "HOLLight.hollight.COS_PI"
  "COS_PERIODIC_PI" > "HOLLight.hollight.COS_PERIODIC_PI"
  "COS_PERIODIC" > "HOLLight.hollight.COS_PERIODIC"
  "COS_PAIRED" > "HOLLight.hollight.COS_PAIRED"
  "COS_ONE_2PI" > "HOLLight.hollight.COS_ONE_2PI"
  "COS_NPI" > "HOLLight.hollight.COS_NPI"
  "COS_NEG" > "HOLLight.hollight.COS_NEG"
  "COS_ISZERO" > "HOLLight.hollight.COS_ISZERO"
  "COS_FDIFF" > "HOLLight.hollight.COS_FDIFF"
  "COS_DOUBLE" > "HOLLight.hollight.COS_DOUBLE"
  "COS_CONVERGES" > "HOLLight.hollight.COS_CONVERGES"
  "COS_BOUNDS" > "HOLLight.hollight.COS_BOUNDS"
  "COS_BOUND" > "HOLLight.hollight.COS_BOUND"
  "COS_ATN_NZ" > "HOLLight.hollight.COS_ATN_NZ"
  "COS_ASN_NZ" > "HOLLight.hollight.COS_ASN_NZ"
  "COS_ADD" > "HOLLight.hollight.COS_ADD"
  "COS_ACS" > "HOLLight.hollight.COS_ACS"
  "COS_ABS" > "HOLLight.hollight.COS_ABS"
  "COS_2" > "HOLLight.hollight.COS_2"
  "COS_0" > "HOLLight.hollight.COS_0"
  "CONT_X" > "HOLLight.hollight.CONT_X"
  "CONT_SUB" > "HOLLight.hollight.CONT_SUB"
  "CONT_NEG" > "HOLLight.hollight.CONT_NEG"
  "CONT_MUL" > "HOLLight.hollight.CONT_MUL"
  "CONT_INVERSE" > "HOLLight.hollight.CONT_INVERSE"
  "CONT_INV" > "HOLLight.hollight.CONT_INV"
  "CONT_INJ_RANGE" > "HOLLight.hollight.CONT_INJ_RANGE"
  "CONT_INJ_LEMMA2" > "HOLLight.hollight.CONT_INJ_LEMMA2"
  "CONT_INJ_LEMMA" > "HOLLight.hollight.CONT_INJ_LEMMA"
  "CONT_HASSUP" > "HOLLight.hollight.CONT_HASSUP"
  "CONT_DIV" > "HOLLight.hollight.CONT_DIV"
  "CONT_CONST" > "HOLLight.hollight.CONT_CONST"
  "CONT_COMPOSE" > "HOLLight.hollight.CONT_COMPOSE"
  "CONT_BOUNDED_ABS" > "HOLLight.hollight.CONT_BOUNDED_ABS"
  "CONT_BOUNDED" > "HOLLight.hollight.CONT_BOUNDED"
  "CONT_ATTAINS_ALL" > "HOLLight.hollight.CONT_ATTAINS_ALL"
  "CONT_ATTAINS2" > "HOLLight.hollight.CONT_ATTAINS2"
  "CONT_ATTAINS" > "HOLLight.hollight.CONT_ATTAINS"
  "CONT_ADD" > "HOLLight.hollight.CONT_ADD"
  "CONTL_LIM" > "HOLLight.hollight.CONTL_LIM"
  "CONS_def" > "HOLLight.hollight.CONS_def"
  "CONS_11" > "HOLLight.hollight.CONS_11"
  "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" > "HOL.conj_comms_1"
  "CONJ_ASSOC" > "HOL.conj_assoc"
  "CONJ_ACI" > "HOLLight.hollight.CONJ_ACI"
  "COND_def" > "HOLLight.hollight.COND_def"
  "COND_RATOR" > "HOLLight.hollight.COND_RATOR"
  "COND_RAND" > "HOLLight.hollight.COND_RAND"
  "COND_ID" > "HOLLight.hollight.COND_ID"
  "COND_EXPAND" > "HOLLight.hollight.COND_EXPAND"
  "COND_EQ_CLAUSE" > "HOLLight.hollight.COND_EQ_CLAUSE"
  "COND_ELIM_THM" > "HOLLight.hollight.COND_ELIM_THM"
  "COND_CLAUSES" > "HOLLight.hollight.COND_CLAUSES"
  "COND_ABS" > "HOLLight.hollight.COND_ABS"
  "COMPONENT" > "HOLLight.hollight.COMPONENT"
  "COMPL_MEM" > "HOLLight.hollight.COMPL_MEM"
  "CLOSED_LIMPT" > "HOLLight.hollight.CLOSED_LIMPT"
  "CIRCLE_SINCOS" > "HOLLight.hollight.CIRCLE_SINCOS"
  "CHOOSE_SUBSET" > "HOLLight.hollight.CHOOSE_SUBSET"
  "CHOICE_def" > "HOLLight.hollight.CHOICE_def"
  "CHOICE_DEF" > "HOLLight.hollight.CHOICE_DEF"
  "CASEWISE_def" > "HOLLight.hollight.CASEWISE_def"
  "CASEWISE_WORKS" > "HOLLight.hollight.CASEWISE_WORKS"
  "CASEWISE_CASES" > "HOLLight.hollight.CASEWISE_CASES"
  "CASEWISE" > "HOLLight.hollight.CASEWISE"
  "CART_EQ" > "HOLLight.hollight.CART_EQ"
  "CARD_def" > "HOLLight.hollight.CARD_def"
  "CARD_UNION_LE" > "HOLLight.hollight.CARD_UNION_LE"
  "CARD_UNION_EQ" > "HOLLight.hollight.CARD_UNION_EQ"
  "CARD_UNIONS_LE" > "HOLLight.hollight.CARD_UNIONS_LE"
  "CARD_UNION" > "HOLLight.hollight.CARD_UNION"
  "CARD_SUBSET_LE" > "HOLLight.hollight.CARD_SUBSET_LE"
  "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_LT_def" > "HOLLight.hollight.CARD_LT_def"
  "CARD_LE_def" > "HOLLight.hollight.CARD_LE_def"
  "CARD_LE_INJ" > "HOLLight.hollight.CARD_LE_INJ"
  "CARD_IMAGE_LE" > "HOLLight.hollight.CARD_IMAGE_LE"
  "CARD_IMAGE_INJ" > "HOLLight.hollight.CARD_IMAGE_INJ"
  "CARD_GT_def" > "HOLLight.hollight.CARD_GT_def"
  "CARD_GE_def" > "HOLLight.hollight.CARD_GE_def"
  "CARD_GE_TRANS" > "HOLLight.hollight.CARD_GE_TRANS"
  "CARD_GE_REFL" > "HOLLight.hollight.CARD_GE_REFL"
  "CARD_FUNSPACE" > "HOLLight.hollight.CARD_FUNSPACE"
  "CARD_FINITE_IMAGE" > "HOLLight.hollight.CARD_FINITE_IMAGE"
  "CARD_EQ_def" > "HOLLight.hollight.CARD_EQ_def"
  "CARD_EQ_SUM" > "HOLLight.hollight.CARD_EQ_SUM"
  "CARD_EQ_NSUM" > "HOLLight.hollight.CARD_EQ_NSUM"
  "CARD_EQ_0" > "HOLLight.hollight.CARD_EQ_0"
  "CARD_DELETE" > "HOLLight.hollight.CARD_DELETE"
  "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" > "Datatype.bool.nchotomy"
  "BOLZANO_LEMMA" > "HOLLight.hollight.BOLZANO_LEMMA"
  "BIT1_THM" > "HOLLightCompat.NUMERAL_BIT1_altdef"
  "BIT0_THM" > "HOLLightCompat.NUMERAL_BIT0_def"
  "BIJ_def" > "HOLLight.hollight.BIJ_def"
  "BETA_THM" > "Presburger.fm_modd_pinf"
  "BALL_OPEN" > "HOLLight.hollight.BALL_OPEN"
  "BALL_NEIGH" > "HOLLight.hollight.BALL_NEIGH"
  "ATN_TAN" > "HOLLight.hollight.ATN_TAN"
  "ATN_POS_LT" > "HOLLight.hollight.ATN_POS_LT"
  "ATN_POS_LE" > "HOLLight.hollight.ATN_POS_LE"
  "ATN_NEG" > "HOLLight.hollight.ATN_NEG"
  "ATN_MONO_LT_EQ" > "HOLLight.hollight.ATN_MONO_LT_EQ"
  "ATN_MONO_LT" > "HOLLight.hollight.ATN_MONO_LT"
  "ATN_MONO_LE_EQ" > "HOLLight.hollight.ATN_MONO_LE_EQ"
  "ATN_LT_PI4_POS" > "HOLLight.hollight.ATN_LT_PI4_POS"
  "ATN_LT_PI4_NEG" > "HOLLight.hollight.ATN_LT_PI4_NEG"
  "ATN_LT_PI4" > "HOLLight.hollight.ATN_LT_PI4"
  "ATN_LE_PI4" > "HOLLight.hollight.ATN_LE_PI4"
  "ATN_INJ" > "HOLLight.hollight.ATN_INJ"
  "ATN_BOUNDS" > "HOLLight.hollight.ATN_BOUNDS"
  "ATN_1" > "HOLLight.hollight.ATN_1"
  "ATN_0" > "HOLLight.hollight.ATN_0"
  "ATN" > "HOLLight.hollight.ATN"
  "ASSOC_def" > "HOLLight.hollight.ASSOC_def"
  "ASN_SIN" > "HOLLight.hollight.ASN_SIN"
  "ASN_BOUNDS_LT" > "HOLLight.hollight.ASN_BOUNDS_LT"
  "ASN_BOUNDS" > "HOLLight.hollight.ASN_BOUNDS"
  "ASN" > "HOLLight.hollight.ASN"
  "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_def" > "HOLLight.hollight.APPEND_def"
  "APPEND_NIL" > "HOLLight.hollight.APPEND_NIL"
  "APPEND_EQ_NIL" > "HOLLight.hollight.APPEND_EQ_NIL"
  "APPEND_ASSOC" > "HOLLight.hollight.APPEND_ASSOC"
  "AND_FORALL_THM" > "HOL.all_conj_distrib"
  "AND_CLAUSES" > "HOLLight.hollight.AND_CLAUSES"
  "AND_ALL2" > "HOLLight.hollight.AND_ALL2"
  "AND_ALL" > "HOLLight.hollight.AND_ALL"
  "ALL_list_def" > "HOLLight.hollight.ALL_list_def"
  "ALL_T" > "HOLLight.hollight.ALL_T"
  "ALL_MP" > "HOLLight.hollight.ALL_MP"
  "ALL_MEM" > "HOLLight.hollight.ALL_MEM"
  "ALL_MAP" > "HOLLight.hollight.ALL_MAP"
  "ALL_IMP" > "HOLLight.hollight.ALL_IMP"
  "ALL_APPEND" > "HOLLight.hollight.ALL_APPEND"
  "ALL2_def" > "HOLLight.hollight.ALL2_def"
  "ALL2_MAP2" > "HOLLight.hollight.ALL2_MAP2"
  "ALL2_MAP" > "HOLLight.hollight.ALL2_MAP"
  "ALL2_AND_RIGHT" > "HOLLight.hollight.ALL2_AND_RIGHT"
  "ALL2_ALL" > "HOLLight.hollight.ALL2_ALL"
  "ALL2" > "HOLLight.hollight.ALL2"
  "ADMISSIBLE_NEST" > "HOLLight.hollight.ADMISSIBLE_NEST"
  "ADMISSIBLE_LAMBDA" > "HOLLight.hollight.ADMISSIBLE_LAMBDA"
  "ADMISSIBLE_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.ADMISSIBLE_IMP_SUPERADMISSIBLE"
  "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" > "Finite_Set.AC_add.f.AC_2"
  "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" > "Finite_Set.AC_add.f.AC_1"
  "ADD_AC" > "HOLLight.hollight.ADD_AC"
  "ADD_0" > "Finite_Set.AC_add.f_e.ident"
  "ADD1" > "HOLLight.hollight.ADD1"
  "ACS_MONO_LT" > "HOLLight.hollight.ACS_MONO_LT"
  "ACS_COS" > "HOLLight.hollight.ACS_COS"
  "ACS_BOUNDS_LT" > "HOLLight.hollight.ACS_BOUNDS_LT"
  "ACS_BOUNDS" > "HOLLight.hollight.ACS_BOUNDS"
  "ACS" > "HOLLight.hollight.ACS"
  "ABS_ZERO" > "HOLLight.hollight.ABS_ZERO"
  "ABS_TRIANGLE" > "HOLLight.hollight.ABS_TRIANGLE"
  "ABS_SUM" > "HOLLight.hollight.ABS_SUM"
  "ABS_SUB_ABS" > "HOLLight.hollight.ABS_SUB_ABS"
  "ABS_SUB" > "HOLLight.hollight.ABS_SUB"
  "ABS_STILLNZ" > "HOLLight.hollight.ABS_STILLNZ"
  "ABS_SIMP" > "Presburger.fm_modd_pinf"
  "ABS_SIGN2" > "HOLLight.hollight.ABS_SIGN2"
  "ABS_SIGN" > "HOLLight.hollight.ABS_SIGN"
  "ABS_REFL" > "HOLLight.hollight.ABS_REFL"
  "ABS_POW2" > "HOLLight.hollight.ABS_POW2"
  "ABS_POS" > "HOLLight.hollight.ABS_POS"
  "ABS_NZ" > "HOLLight.hollight.ABS_NZ"
  "ABS_NEG_LEMMA" > "HOLLight.hollight.ABS_NEG_LEMMA"
  "ABS_NEG" > "HOLLight.hollight.ABS_NEG"
  "ABS_N" > "HOLLight.hollight.ABS_N"
  "ABS_MUL" > "HOLLight.hollight.ABS_MUL"
  "ABS_LT_MUL2" > "HOLLight.hollight.ABS_LT_MUL2"
  "ABS_LE" > "HOLLight.hollight.ABS_LE"
  "ABS_INV" > "HOLLight.hollight.ABS_INV"
  "ABS_DIV" > "HOLLight.hollight.ABS_DIV"
  "ABS_CIRCLE" > "HOLLight.hollight.ABS_CIRCLE"
  "ABS_CASES" > "HOLLight.hollight.ABS_CASES"
  "ABS_BOUNDS" > "HOLLight.hollight.ABS_BOUNDS"
  "ABS_BOUND" > "HOLLight.hollight.ABS_BOUND"
  "ABS_BETWEEN2" > "HOLLight.hollight.ABS_BETWEEN2"
  "ABS_BETWEEN1" > "HOLLight.hollight.ABS_BETWEEN1"
  "ABS_BETWEEN" > "HOLLight.hollight.ABS_BETWEEN"
  "ABS_ABS" > "HOLLight.hollight.ABS_ABS"
  "ABS_1" > "HOLLight.hollight.ABS_1"
  "ABS_0" > "HOLLight.hollight.ABS_0"
  "ABSORPTION" > "HOLLight.hollight.ABSORPTION"
  ">_def" > "HOLLight.hollight.>_def"
  ">=_def" > "HOLLight.hollight.>=_def"
  "<_def" > "HOLLight.hollight.<_def"
  "<=_def" > "HOLLight.hollight.<=_def"
  "$_def" > "HOLLight.hollight.$_def"

ignore_thms
  "TYDEF_prod"
  "TYDEF_num"
  "TYDEF_1"
  "IND_SUC_0_EXISTS"
  "DEF_one"
  "DEF__0"
  "DEF_SUC"
  "DEF_NUM_REP"
  "DEF_IND_SUC"
  "DEF_IND_0"

end