src/HOL/Import/HOLLight/hollight.imp
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 39302 d7728f65b353
child 43786 fea3ed6951e3
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 import
     2 
     3 import_segment "hollight"
     4 
     5 type_maps
     6   "sum" > "+"
     7   "recspace" > "HOLLight.hollight.recspace"
     8   "real" > "HOLLight.hollight.real"
     9   "prod" > "Product_Type.prod"
    10   "option" > "HOLLight.hollight.option"
    11   "num" > "Nat.nat"
    12   "nadd" > "HOLLight.hollight.nadd"
    13   "list" > "HOLLight.hollight.list"
    14   "int" > "HOLLight.hollight.int"
    15   "ind" > "Nat.ind"
    16   "hreal" > "HOLLight.hollight.hreal"
    17   "fun" > "fun"
    18   "finite_sum" > "HOLLight.hollight.finite_sum"
    19   "finite_image" > "HOLLight.hollight.finite_image"
    20   "cart" > "HOLLight.hollight.cart"
    21   "bool" > "HOL.bool"
    22   "N_3" > "HOLLight.hollight.N_3"
    23   "N_2" > "HOLLight.hollight.N_2"
    24   "N_1" > "Product_Type.unit"
    25 
    26 const_maps
    27   "~" > "HOL.Not"
    28   "two_2" > "HOLLight.hollight.two_2"
    29   "two_1" > "HOLLight.hollight.two_1"
    30   "treal_of_num" > "HOLLight.hollight.treal_of_num"
    31   "treal_neg" > "HOLLight.hollight.treal_neg"
    32   "treal_mul" > "HOLLight.hollight.treal_mul"
    33   "treal_le" > "HOLLight.hollight.treal_le"
    34   "treal_inv" > "HOLLight.hollight.treal_inv"
    35   "treal_eq" > "HOLLight.hollight.treal_eq"
    36   "treal_add" > "HOLLight.hollight.treal_add"
    37   "three_3" > "HOLLight.hollight.three_3"
    38   "three_2" > "HOLLight.hollight.three_2"
    39   "three_1" > "HOLLight.hollight.three_1"
    40   "tailadmissible" > "HOLLight.hollight.tailadmissible"
    41   "support" > "HOLLight.hollight.support"
    42   "superadmissible" > "HOLLight.hollight.superadmissible"
    43   "sum" > "HOLLight.hollight.sum"
    44   "sndcart" > "HOLLight.hollight.sndcart"
    45   "set_of_list" > "HOLLight.hollight.set_of_list"
    46   "real_sub" > "HOLLight.hollight.real_sub"
    47   "real_pow" > "HOLLight.hollight.real_pow"
    48   "real_of_num" > "HOLLight.hollight.real_of_num"
    49   "real_neg" > "HOLLight.hollight.real_neg"
    50   "real_mul" > "HOLLight.hollight.real_mul"
    51   "real_min" > "HOLLight.hollight.real_min"
    52   "real_max" > "HOLLight.hollight.real_max"
    53   "real_lt" > "HOLLight.hollight.real_lt"
    54   "real_le" > "HOLLight.hollight.real_le"
    55   "real_inv" > "HOLLight.hollight.real_inv"
    56   "real_gt" > "HOLLight.hollight.real_gt"
    57   "real_ge" > "HOLLight.hollight.real_ge"
    58   "real_div" > "HOLLight.hollight.real_div"
    59   "real_add" > "HOLLight.hollight.real_add"
    60   "real_abs" > "HOLLight.hollight.real_abs"
    61   "pastecart" > "HOLLight.hollight.pastecart"
    62   "pairwise" > "HOLLight.hollight.pairwise"
    63   "one" > "Product_Type.Unity"
    64   "o" > "Fun.comp"
    65   "nsum" > "HOLLight.hollight.nsum"
    66   "neutral" > "HOLLight.hollight.neutral"
    67   "nadd_rinv" > "HOLLight.hollight.nadd_rinv"
    68   "nadd_of_num" > "HOLLight.hollight.nadd_of_num"
    69   "nadd_mul" > "HOLLight.hollight.nadd_mul"
    70   "nadd_le" > "HOLLight.hollight.nadd_le"
    71   "nadd_inv" > "HOLLight.hollight.nadd_inv"
    72   "nadd_eq" > "HOLLight.hollight.nadd_eq"
    73   "nadd_add" > "HOLLight.hollight.nadd_add"
    74   "monoidal" > "HOLLight.hollight.monoidal"
    75   "mod_real" > "HOLLight.hollight.mod_real"
    76   "mod_nat" > "HOLLight.hollight.mod_nat"
    77   "mod_int" > "HOLLight.hollight.mod_int"
    78   "mk_pair" > "Product_Type.Pair_Rep"
    79   "minimal" > "HOLLight.hollight.minimal"
    80   "measure" > "HOLLight.hollight.measure"
    81   "list_of_set" > "HOLLight.hollight.list_of_set"
    82   "lambda" > "HOLLight.hollight.lambda"
    83   "iterate" > "HOLLight.hollight.iterate"
    84   "is_nadd" > "HOLLight.hollight.is_nadd"
    85   "is_int" > "HOLLight.hollight.is_int"
    86   "int_sub" > "HOLLight.hollight.int_sub"
    87   "int_pow" > "HOLLight.hollight.int_pow"
    88   "int_of_num" > "HOLLight.hollight.int_of_num"
    89   "int_neg" > "HOLLight.hollight.int_neg"
    90   "int_mul" > "HOLLight.hollight.int_mul"
    91   "int_min" > "HOLLight.hollight.int_min"
    92   "int_max" > "HOLLight.hollight.int_max"
    93   "int_lt" > "HOLLight.hollight.int_lt"
    94   "int_le" > "HOLLight.hollight.int_le"
    95   "int_gt" > "HOLLight.hollight.int_gt"
    96   "int_ge" > "HOLLight.hollight.int_ge"
    97   "int_add" > "HOLLight.hollight.int_add"
    98   "int_abs" > "HOLLight.hollight.int_abs"
    99   "hreal_of_num" > "HOLLight.hollight.hreal_of_num"
   100   "hreal_mul" > "HOLLight.hollight.hreal_mul"
   101   "hreal_le" > "HOLLight.hollight.hreal_le"
   102   "hreal_inv" > "HOLLight.hollight.hreal_inv"
   103   "hreal_add" > "HOLLight.hollight.hreal_add"
   104   "fstcart" > "HOLLight.hollight.fstcart"
   105   "finite_index" > "HOLLight.hollight.finite_index"
   106   "eqeq" > "HOLLight.hollight.eqeq"
   107   "dotdot" > "HOLLight.hollight.dotdot"
   108   "dist" > "HOLLight.hollight.dist"
   109   "dimindex" > "HOLLight.hollight.dimindex"
   110   "admissible" > "HOLLight.hollight.admissible"
   111   "_FALSITY_" > "HOLLight.hollight._FALSITY_"
   112   "_10328" > "HOLLight.hollight._10328"
   113   "_10327" > "HOLLight.hollight._10327"
   114   "_10326" > "HOLLight.hollight._10326"
   115   "_10303" > "HOLLight.hollight._10303"
   116   "_10302" > "HOLLight.hollight._10302"
   117   "_0" > "0" :: "nat"
   118   "\\/" > HOL.disj
   119   "ZRECSPACE" > "HOLLight.hollight.ZRECSPACE"
   120   "ZIP" > "HOLLight.hollight.ZIP"
   121   "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
   122   "ZBOT" > "HOLLight.hollight.ZBOT"
   123   "WF" > "HOLLight.hollight.WF"
   124   "UNIV" > "HOLLight.hollight.UNIV"
   125   "UNIONS" > "HOLLight.hollight.UNIONS"
   126   "UNION" > "HOLLight.hollight.UNION"
   127   "UNCURRY" > "HOLLight.hollight.UNCURRY"
   128   "TL" > "HOLLight.hollight.TL"
   129   "T" > "True"
   130   "SURJ" > "HOLLight.hollight.SURJ"
   131   "SUC" > "Nat.Suc"
   132   "SUBSET" > "HOLLight.hollight.SUBSET"
   133   "SOME" > "HOLLight.hollight.SOME"
   134   "SND" > "Product_Type.snd"
   135   "SING" > "HOLLight.hollight.SING"
   136   "SETSPEC" > "HOLLight.hollight.SETSPEC"
   137   "REVERSE" > "HOLLight.hollight.REVERSE"
   138   "REST" > "HOLLight.hollight.REST"
   139   "REP_prod" > "Rep_Prod"
   140   "REPLICATE" > "HOLLight.hollight.REPLICATE"
   141   "PSUBSET" > "HOLLight.hollight.PSUBSET"
   142   "PRE" > "HOLLightCompat.Pred"
   143   "PASSOC" > "HOLLight.hollight.PASSOC"
   144   "PAIRWISE" > "HOLLight.hollight.PAIRWISE"
   145   "OUTR" > "HOLLight.hollight.OUTR"
   146   "OUTL" > "HOLLight.hollight.OUTL"
   147   "ONTO" > "Fun.surj"
   148   "ONE_ONE" > "HOL4Setup.ONE_ONE"
   149   "ODD" > "HOLLight.hollight.ODD"
   150   "NUMSUM" > "HOLLight.hollight.NUMSUM"
   151   "NUMSND" > "HOLLight.hollight.NUMSND"
   152   "NUMRIGHT" > "HOLLight.hollight.NUMRIGHT"
   153   "NUMPAIR" > "HOLLight.hollight.NUMPAIR"
   154   "NUMLEFT" > "HOLLight.hollight.NUMLEFT"
   155   "NUMFST" > "HOLLight.hollight.NUMFST"
   156   "NUMERAL" > "HOL4Compat.NUMERAL"
   157   "NULL" > "HOLLight.hollight.NULL"
   158   "NONE" > "HOLLight.hollight.NONE"
   159   "NIL" > "HOLLight.hollight.NIL"
   160   "MOD" > "HOLLight.hollight.MOD"
   161   "MEM" > "HOLLight.hollight.MEM"
   162   "MAP2" > "HOLLight.hollight.MAP2"
   163   "MAP" > "HOLLight.hollight.MAP"
   164   "LET_END" > "HOLLight.hollight.LET_END"
   165   "LET" > "HOL4Compat.LET"
   166   "LENGTH" > "HOLLight.hollight.LENGTH"
   167   "LAST" > "HOLLight.hollight.LAST"
   168   "ITSET" > "HOLLight.hollight.ITSET"
   169   "ITLIST2" > "HOLLight.hollight.ITLIST2"
   170   "ITLIST" > "HOLLight.hollight.ITLIST"
   171   "ISO" > "HOLLight.hollight.ISO"
   172   "INTERS" > "HOLLight.hollight.INTERS"
   173   "INTER" > "HOLLight.hollight.INTER"
   174   "INSERT" > "HOLLight.hollight.INSERT"
   175   "INR" > "Sum_Type.Inr"
   176   "INL" > "Sum_Type.Inl"
   177   "INJP" > "HOLLight.hollight.INJP"
   178   "INJN" > "HOLLight.hollight.INJN"
   179   "INJF" > "HOLLight.hollight.INJF"
   180   "INJA" > "HOLLight.hollight.INJA"
   181   "INJ" > "HOLLight.hollight.INJ"
   182   "INFINITE" > "HOLLight.hollight.INFINITE"
   183   "IN" > "HOLLight.hollight.IN"
   184   "IMAGE" > "HOLLight.hollight.IMAGE"
   185   "I" > "Fun.id"
   186   "HD" > "HOLLight.hollight.HD"
   187   "HAS_SIZE" > "HOLLight.hollight.HAS_SIZE"
   188   "GSPEC" > "HOLLight.hollight.GSPEC"
   189   "GEQ" > "HOLLight.hollight.GEQ"
   190   "GABS" > "HOLLight.hollight.GABS"
   191   "FST" > "Product_Type.fst"
   192   "FNIL" > "HOLLight.hollight.FNIL"
   193   "FINREC" > "HOLLight.hollight.FINREC"
   194   "FINITE" > "HOLLight.hollight.FINITE"
   195   "FILTER" > "HOLLight.hollight.FILTER"
   196   "FCONS" > "HOLLight.hollight.FCONS"
   197   "FACT" > "HOLLight.hollight.FACT"
   198   "F" > "False"
   199   "EXP" > "HOLLight.hollight.EXP"
   200   "EX" > "HOLLight.hollight.EX"
   201   "EVEN" > "HOLLight.hollight.EVEN"
   202   "EMPTY" > "HOLLight.hollight.EMPTY"
   203   "EL" > "HOLLight.hollight.EL"
   204   "DIV" > "HOLLight.hollight.DIV"
   205   "DISJOINT" > "HOLLight.hollight.DISJOINT"
   206   "DIFF" > "HOLLight.hollight.DIFF"
   207   "DELETE" > "HOLLight.hollight.DELETE"
   208   "DECIMAL" > "HOLLight.hollight.DECIMAL"
   209   "CURRY" > "HOLLight.hollight.CURRY"
   210   "COUNTABLE" > "HOLLight.hollight.COUNTABLE"
   211   "CONSTR" > "HOLLight.hollight.CONSTR"
   212   "CONS" > "HOLLight.hollight.CONS"
   213   "COND" > "HOLLight.hollight.COND"
   214   "CHOICE" > "HOLLight.hollight.CHOICE"
   215   "CASEWISE" > "HOLLight.hollight.CASEWISE"
   216   "CARD_LT" > "HOLLight.hollight.CARD_LT"
   217   "CARD_LE" > "HOLLight.hollight.CARD_LE"
   218   "CARD_GT" > "HOLLight.hollight.CARD_GT"
   219   "CARD_GE" > "HOLLight.hollight.CARD_GE"
   220   "CARD_EQ" > "HOLLight.hollight.CARD_EQ"
   221   "CARD" > "HOLLight.hollight.CARD"
   222   "BOTTOM" > "HOLLight.hollight.BOTTOM"
   223   "BIT1" > "HOL4Compat.NUMERAL_BIT1"
   224   "BIT0" > "HOLLightCompat.NUMERAL_BIT0"
   225   "BIJ" > "HOLLight.hollight.BIJ"
   226   "ASSOC" > "HOLLight.hollight.ASSOC"
   227   "APPEND" > "HOLLight.hollight.APPEND"
   228   "ALL_list" > "HOLLight.hollight.ALL_list"
   229   "ALL2" > "HOLLight.hollight.ALL2"
   230   "ABS_prod" > "Abs_Prod"
   231   "@" > "Hilbert_Choice.Eps"
   232   "?!" > "HOL.Ex1"
   233   "?" > "HOL.Ex"
   234   ">=" > "HOLLight.hollight.>="
   235   ">" > "HOLLight.hollight.>"
   236   "==>" > HOL.implies
   237   "=" > HOL.eq
   238   "<=" > "HOLLight.hollight.<="
   239   "<" > "HOLLight.hollight.<"
   240   "/\\" > HOL.conj
   241   "-" > "Groups.minus" :: "nat => nat => nat"
   242   "," > "Product_Type.Pair"
   243   "+" > "Groups.plus" :: "nat => nat => nat"
   244   "*" > "Groups.times" :: "nat => nat => nat"
   245   "$" > "HOLLight.hollight.$"
   246   "!" > "HOL.All"
   247 
   248 const_renames
   249   "ALL" > "ALL_list"
   250   "==" > "eqeq"
   251   ".." > "dotdot"
   252 
   253 thm_maps
   254   "two_2_def" > "HOLLight.hollight.two_2_def"
   255   "two_1_def" > "HOLLight.hollight.two_1_def"
   256   "treal_of_num_def" > "HOLLight.hollight.treal_of_num_def"
   257   "treal_neg_def" > "HOLLight.hollight.treal_neg_def"
   258   "treal_mul_def" > "HOLLight.hollight.treal_mul_def"
   259   "treal_le_def" > "HOLLight.hollight.treal_le_def"
   260   "treal_inv_def" > "HOLLight.hollight.treal_inv_def"
   261   "treal_eq_def" > "HOLLight.hollight.treal_eq_def"
   262   "treal_add_def" > "HOLLight.hollight.treal_add_def"
   263   "three_3_def" > "HOLLight.hollight.three_3_def"
   264   "three_2_def" > "HOLLight.hollight.three_2_def"
   265   "three_1_def" > "HOLLight.hollight.three_1_def"
   266   "th_cond" > "HOLLight.hollight.th_cond"
   267   "th" > "Fun.id_apply"
   268   "tailadmissible_def" > "HOLLight.hollight.tailadmissible_def"
   269   "support_def" > "HOLLight.hollight.support_def"
   270   "superadmissible_def" > "HOLLight.hollight.superadmissible_def"
   271   "sum_def" > "HOLLight.hollight.sum_def"
   272   "sum_RECURSION" > "HOLLightCompat.sum_Recursion"
   273   "sum_INDUCT" > "HOLLightCompat.sumlift.induct"
   274   "sth" > "HOLLight.hollight.sth"
   275   "sndcart_def" > "HOLLight.hollight.sndcart_def"
   276   "set_of_list_def" > "HOLLight.hollight.set_of_list_def"
   277   "right_th" > "HOLLight.hollight.right_th"
   278   "real_sub_def" > "HOLLight.hollight.real_sub_def"
   279   "real_pow_def" > "HOLLight.hollight.real_pow_def"
   280   "real_of_num_def" > "HOLLight.hollight.real_of_num_def"
   281   "real_neg_def" > "HOLLight.hollight.real_neg_def"
   282   "real_mul_def" > "HOLLight.hollight.real_mul_def"
   283   "real_min_def" > "HOLLight.hollight.real_min_def"
   284   "real_max_def" > "HOLLight.hollight.real_max_def"
   285   "real_lt_def" > "HOLLight.hollight.real_lt_def"
   286   "real_le_def" > "HOLLight.hollight.real_le_def"
   287   "real_inv_def" > "HOLLight.hollight.real_inv_def"
   288   "real_gt_def" > "HOLLight.hollight.real_gt_def"
   289   "real_ge_def" > "HOLLight.hollight.real_ge_def"
   290   "real_div_def" > "HOLLight.hollight.real_div_def"
   291   "real_add_def" > "HOLLight.hollight.real_add_def"
   292   "real_abs_def" > "HOLLight.hollight.real_abs_def"
   293   "pastecart_def" > "HOLLight.hollight.pastecart_def"
   294   "pairwise_def" > "HOLLight.hollight.pairwise_def"
   295   "pair_RECURSION" > "HOLLight.hollight.pair_RECURSION"
   296   "pair_INDUCT" > "Datatype.prod.inducts"
   297   "one_axiom" > "HOLLight.hollight.one_axiom"
   298   "one_RECURSION" > "HOLLight.hollight.one_RECURSION"
   299   "one_INDUCT" > "Datatype.unit.inducts"
   300   "one_Axiom" > "HOLLight.hollight.one_Axiom"
   301   "one" > "HOL4Compat.one"
   302   "o_THM" > "Fun.o_apply"
   303   "o_ASSOC" > "HOLLight.hollight.o_ASSOC"
   304   "num_WOP" > "HOLLight.hollight.num_WOP"
   305   "num_WF" > "HOLLight.hollight.num_WF"
   306   "num_RECURSION_STD" > "HOLLight.hollight.num_RECURSION_STD"
   307   "num_MAX" > "HOLLight.hollight.num_MAX"
   308   "num_INFINITE" > "HOLLight.hollight.num_INFINITE"
   309   "num_INDUCTION" > "List.lexn.induct"
   310   "num_FINITE_AVOID" > "HOLLight.hollight.num_FINITE_AVOID"
   311   "num_FINITE" > "HOLLight.hollight.num_FINITE"
   312   "num_CASES" > "Nat.nat.nchotomy"
   313   "num_Axiom" > "HOLLight.hollight.num_Axiom"
   314   "nsum_def" > "HOLLight.hollight.nsum_def"
   315   "neutral_def" > "HOLLight.hollight.neutral_def"
   316   "nadd_rinv_def" > "HOLLight.hollight.nadd_rinv_def"
   317   "nadd_of_num_def" > "HOLLight.hollight.nadd_of_num_def"
   318   "nadd_mul_def" > "HOLLight.hollight.nadd_mul_def"
   319   "nadd_le_def" > "HOLLight.hollight.nadd_le_def"
   320   "nadd_inv_def" > "HOLLight.hollight.nadd_inv_def"
   321   "nadd_eq_def" > "HOLLight.hollight.nadd_eq_def"
   322   "nadd_add_def" > "HOLLight.hollight.nadd_add_def"
   323   "monoidal_def" > "HOLLight.hollight.monoidal_def"
   324   "mod_real_def" > "HOLLight.hollight.mod_real_def"
   325   "mod_nat_def" > "HOLLight.hollight.mod_nat_def"
   326   "mod_int_def" > "HOLLight.hollight.mod_int_def"
   327   "minimal_def" > "HOLLight.hollight.minimal_def"
   328   "measure_def" > "HOLLight.hollight.measure_def"
   329   "list_of_set_def" > "HOLLight.hollight.list_of_set_def"
   330   "list_INDUCT" > "HOLLight.hollight.list_INDUCT"
   331   "list_CASES" > "HOLLight.hollight.list_CASES"
   332   "lambda_def" > "HOLLight.hollight.lambda_def"
   333   "iterate_def" > "HOLLight.hollight.iterate_def"
   334   "is_nadd_def" > "HOLLight.hollight.is_nadd_def"
   335   "is_nadd_0" > "HOLLight.hollight.is_nadd_0"
   336   "is_int_def" > "HOLLight.hollight.is_int_def"
   337   "int_sub_th" > "HOLLight.hollight.int_sub_th"
   338   "int_sub_def" > "HOLLight.hollight.int_sub_def"
   339   "int_pow_th" > "HOLLight.hollight.int_pow_th"
   340   "int_pow_def" > "HOLLight.hollight.int_pow_def"
   341   "int_of_num_th" > "HOLLight.hollight.int_of_num_th"
   342   "int_of_num_def" > "HOLLight.hollight.int_of_num_def"
   343   "int_neg_th" > "HOLLight.hollight.int_neg_th"
   344   "int_neg_def" > "HOLLight.hollight.int_neg_def"
   345   "int_mul_th" > "HOLLight.hollight.int_mul_th"
   346   "int_mul_def" > "HOLLight.hollight.int_mul_def"
   347   "int_min_th" > "HOLLight.hollight.int_min_th"
   348   "int_min_def" > "HOLLight.hollight.int_min_def"
   349   "int_max_th" > "HOLLight.hollight.int_max_th"
   350   "int_max_def" > "HOLLight.hollight.int_max_def"
   351   "int_lt_def" > "HOLLight.hollight.int_lt_def"
   352   "int_le_def" > "HOLLight.hollight.int_le_def"
   353   "int_gt_def" > "HOLLight.hollight.int_gt_def"
   354   "int_ge_def" > "HOLLight.hollight.int_ge_def"
   355   "int_eq" > "HOLLight.hollight.int.dest_int_inject"
   356   "int_add_th" > "HOLLight.hollight.int_add_th"
   357   "int_add_def" > "HOLLight.hollight.int_add_def"
   358   "int_abs_th" > "HOLLight.hollight.int_abs_th"
   359   "int_abs_def" > "HOLLight.hollight.int_abs_def"
   360   "hreal_of_num_def" > "HOLLight.hollight.hreal_of_num_def"
   361   "hreal_mul_def" > "HOLLight.hollight.hreal_mul_def"
   362   "hreal_le_def" > "HOLLight.hollight.hreal_le_def"
   363   "hreal_inv_def" > "HOLLight.hollight.hreal_inv_def"
   364   "hreal_add_def" > "HOLLight.hollight.hreal_add_def"
   365   "fstcart_def" > "HOLLight.hollight.fstcart_def"
   366   "finite_index_def" > "HOLLight.hollight.finite_index_def"
   367   "eqeq_def" > "HOLLight.hollight.eqeq_def"
   368   "dotdot_def" > "HOLLight.hollight.dotdot_def"
   369   "dist_def" > "HOLLight.hollight.dist_def"
   370   "dimindex_def" > "HOLLight.hollight.dimindex_def"
   371   "dest_int_rep" > "HOLLight.hollight.dest_int_rep"
   372   "cth" > "HOLLight.hollight.cth"
   373   "bool_RECURSION" > "HOLLight.hollight.bool_RECURSION"
   374   "ax__3" > "HOL4Setup.INFINITY_AX"
   375   "ax__2" > "Hilbert_Choice.tfl_some"
   376   "ax__1" > "Presburger.fm_modd_pinf"
   377   "admissible_def" > "HOLLight.hollight.admissible_def"
   378   "_FALSITY__def" > "HOLLight.hollight._FALSITY__def"
   379   "_10328_def" > "HOLLight.hollight._10328_def"
   380   "_10327_def" > "HOLLight.hollight._10327_def"
   381   "_10326_def" > "HOLLight.hollight._10326_def"
   382   "_10303_def" > "HOLLight.hollight._10303_def"
   383   "_10302_def" > "HOLLight.hollight._10302_def"
   384   "ZRECSPACE_def" > "HOLLight.hollight.ZRECSPACE_def"
   385   "ZIP_def" > "HOLLight.hollight.ZIP_def"
   386   "ZIP" > "HOLLight.hollight.ZIP"
   387   "ZCONSTR_def" > "HOLLight.hollight.ZCONSTR_def"
   388   "ZCONSTR_ZBOT" > "HOLLight.hollight.ZCONSTR_ZBOT"
   389   "ZBOT_def" > "HOLLight.hollight.ZBOT_def"
   390   "WLOG_LT" > "HOLLight.hollight.WLOG_LT"
   391   "WLOG_LE" > "HOLLight.hollight.WLOG_LE"
   392   "WF_num" > "HOLLight.hollight.WF_num"
   393   "WF_def" > "HOLLight.hollight.WF_def"
   394   "WF_UREC_WF" > "HOLLight.hollight.WF_UREC_WF"
   395   "WF_UREC" > "HOLLight.hollight.WF_UREC"
   396   "WF_SUBSET" > "HOLLight.hollight.WF_SUBSET"
   397   "WF_REFL" > "HOLLight.hollight.WF_REFL"
   398   "WF_REC_num" > "HOLLight.hollight.WF_REC_num"
   399   "WF_REC_WF" > "HOLLight.hollight.WF_REC_WF"
   400   "WF_REC_TAIL_GENERAL" > "HOLLight.hollight.WF_REC_TAIL_GENERAL"
   401   "WF_REC_TAIL" > "HOLLight.hollight.WF_REC_TAIL"
   402   "WF_REC_INVARIANT" > "HOLLight.hollight.WF_REC_INVARIANT"
   403   "WF_REC_CASES" > "HOLLight.hollight.WF_REC_CASES"
   404   "WF_REC" > "HOLLight.hollight.WF_REC"
   405   "WF_POINTWISE" > "HOLLight.hollight.WF_POINTWISE"
   406   "WF_MEASURE_GEN" > "HOLLight.hollight.WF_MEASURE_GEN"
   407   "WF_MEASURE" > "HOLLight.hollight.WF_MEASURE"
   408   "WF_LEX_DEPENDENT" > "HOLLight.hollight.WF_LEX_DEPENDENT"
   409   "WF_LEX" > "HOLLight.hollight.WF_LEX"
   410   "WF_IND" > "HOLLight.hollight.WF_IND"
   411   "WF_FALSE" > "HOLLight.hollight.WF_FALSE"
   412   "WF_EREC" > "HOLLight.hollight.WF_EREC"
   413   "WF_EQ" > "HOLLight.hollight.WF_EQ"
   414   "WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
   415   "UNWIND_THM2" > "HOL.simp_thms_39"
   416   "UNWIND_THM1" > "HOL.simp_thms_40"
   417   "UNIV_def" > "HOLLight.hollight.UNIV_def"
   418   "UNIV_SUBSET" > "HOLLight.hollight.UNIV_SUBSET"
   419   "UNIV_NOT_EMPTY" > "HOLLight.hollight.UNIV_NOT_EMPTY"
   420   "UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
   421   "UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
   422   "UNION_def" > "HOLLight.hollight.UNION_def"
   423   "UNION_UNIV" > "HOLLight.hollight.UNION_UNIV"
   424   "UNION_SUBSET" > "HOLLight.hollight.UNION_SUBSET"
   425   "UNION_OVER_INTER" > "HOLLight.hollight.UNION_OVER_INTER"
   426   "UNION_IDEMPOT" > "HOLLight.hollight.UNION_IDEMPOT"
   427   "UNION_EMPTY" > "HOLLight.hollight.UNION_EMPTY"
   428   "UNION_COMM" > "HOLLight.hollight.UNION_COMM"
   429   "UNION_ASSOC" > "HOLLight.hollight.UNION_ASSOC"
   430   "UNION_ACI" > "HOLLight.hollight.UNION_ACI"
   431   "UNIONS_def" > "HOLLight.hollight.UNIONS_def"
   432   "UNIONS_INSERT" > "HOLLight.hollight.UNIONS_INSERT"
   433   "UNIONS_2" > "HOLLight.hollight.UNIONS_2"
   434   "UNIONS_1" > "HOLLight.hollight.UNIONS_1"
   435   "UNIONS_0" > "HOLLight.hollight.UNIONS_0"
   436   "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
   437   "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
   438   "TYDEF_real" > "HOLLight.hollight.TYDEF_real"
   439   "TYDEF_option" > "HOLLight.hollight.TYDEF_option"
   440   "TYDEF_nadd" > "HOLLight.hollight.TYDEF_nadd"
   441   "TYDEF_list" > "HOLLight.hollight.TYDEF_list"
   442   "TYDEF_int" > "HOLLight.hollight.TYDEF_int"
   443   "TYDEF_hreal" > "HOLLight.hollight.TYDEF_hreal"
   444   "TYDEF_finite_sum" > "HOLLight.hollight.TYDEF_finite_sum"
   445   "TYDEF_finite_image" > "HOLLight.hollight.TYDEF_finite_image"
   446   "TYDEF_cart" > "HOLLight.hollight.TYDEF_cart"
   447   "TYDEF_3" > "HOLLight.hollight.TYDEF_3"
   448   "TYDEF_2" > "HOLLight.hollight.TYDEF_2"
   449   "TWO" > "HOLLight.hollight.TWO"
   450   "TRIV_OR_FORALL_THM" > "HOLLight.hollight.TRIV_OR_FORALL_THM"
   451   "TRIV_FORALL_OR_THM" > "HOLLight.hollight.TRIV_FORALL_OR_THM"
   452   "TRIV_FORALL_IMP_THM" > "HOLLight.hollight.TRIV_FORALL_IMP_THM"
   453   "TRIV_EXISTS_IMP_THM" > "HOLLight.hollight.TRIV_EXISTS_IMP_THM"
   454   "TRIV_EXISTS_AND_THM" > "HOLLight.hollight.TRIV_EXISTS_AND_THM"
   455   "TRIV_AND_EXISTS_THM" > "HOLLight.hollight.TRIV_AND_EXISTS_THM"
   456   "TREAL_OF_NUM_WELLDEF" > "HOLLight.hollight.TREAL_OF_NUM_WELLDEF"
   457   "TREAL_OF_NUM_MUL" > "HOLLight.hollight.TREAL_OF_NUM_MUL"
   458   "TREAL_OF_NUM_LE" > "HOLLight.hollight.TREAL_OF_NUM_LE"
   459   "TREAL_OF_NUM_EQ" > "HOLLight.hollight.TREAL_OF_NUM_EQ"
   460   "TREAL_OF_NUM_ADD" > "HOLLight.hollight.TREAL_OF_NUM_ADD"
   461   "TREAL_NEG_WELLDEF" > "HOLLight.hollight.TREAL_NEG_WELLDEF"
   462   "TREAL_MUL_WELLDEFR" > "HOLLight.hollight.TREAL_MUL_WELLDEFR"
   463   "TREAL_MUL_WELLDEF" > "HOLLight.hollight.TREAL_MUL_WELLDEF"
   464   "TREAL_MUL_SYM_EQ" > "HOLLight.hollight.TREAL_MUL_SYM_EQ"
   465   "TREAL_MUL_SYM" > "HOLLight.hollight.TREAL_MUL_SYM"
   466   "TREAL_MUL_LINV" > "HOLLight.hollight.TREAL_MUL_LINV"
   467   "TREAL_MUL_LID" > "HOLLight.hollight.TREAL_MUL_LID"
   468   "TREAL_MUL_ASSOC" > "HOLLight.hollight.TREAL_MUL_ASSOC"
   469   "TREAL_LE_WELLDEF" > "HOLLight.hollight.TREAL_LE_WELLDEF"
   470   "TREAL_LE_TRANS" > "HOLLight.hollight.TREAL_LE_TRANS"
   471   "TREAL_LE_TOTAL" > "HOLLight.hollight.TREAL_LE_TOTAL"
   472   "TREAL_LE_REFL" > "HOLLight.hollight.TREAL_LE_REFL"
   473   "TREAL_LE_MUL" > "HOLLight.hollight.TREAL_LE_MUL"
   474   "TREAL_LE_LADD_IMP" > "HOLLight.hollight.TREAL_LE_LADD_IMP"
   475   "TREAL_LE_ANTISYM" > "HOLLight.hollight.TREAL_LE_ANTISYM"
   476   "TREAL_INV_WELLDEF" > "HOLLight.hollight.TREAL_INV_WELLDEF"
   477   "TREAL_INV_0" > "HOLLight.hollight.TREAL_INV_0"
   478   "TREAL_EQ_TRANS" > "HOLLight.hollight.TREAL_EQ_TRANS"
   479   "TREAL_EQ_SYM" > "HOLLight.hollight.TREAL_EQ_SYM"
   480   "TREAL_EQ_REFL" > "HOLLight.hollight.TREAL_EQ_REFL"
   481   "TREAL_EQ_IMP_LE" > "HOLLight.hollight.TREAL_EQ_IMP_LE"
   482   "TREAL_EQ_AP" > "HOLLight.hollight.TREAL_EQ_AP"
   483   "TREAL_ADD_WELLDEFR" > "HOLLight.hollight.TREAL_ADD_WELLDEFR"
   484   "TREAL_ADD_WELLDEF" > "HOLLight.hollight.TREAL_ADD_WELLDEF"
   485   "TREAL_ADD_SYM_EQ" > "HOLLight.hollight.TREAL_ADD_SYM_EQ"
   486   "TREAL_ADD_SYM" > "HOLLight.hollight.TREAL_ADD_SYM"
   487   "TREAL_ADD_LINV" > "HOLLight.hollight.TREAL_ADD_LINV"
   488   "TREAL_ADD_LID" > "HOLLight.hollight.TREAL_ADD_LID"
   489   "TREAL_ADD_LDISTRIB" > "HOLLight.hollight.TREAL_ADD_LDISTRIB"
   490   "TREAL_ADD_ASSOC" > "HOLLight.hollight.TREAL_ADD_ASSOC"
   491   "TL_def" > "HOLLight.hollight.TL_def"
   492   "TAIL_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.TAIL_IMP_SUPERADMISSIBLE"
   493   "SWAP_FORALL_THM" > "HOLLight.hollight.SWAP_FORALL_THM"
   494   "SWAP_EXISTS_THM" > "HOLLight.hollight.SWAP_EXISTS_THM"
   495   "SURJ_def" > "HOLLight.hollight.SURJ_def"
   496   "SURJECTIVE_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_RIGHT_INVERSE"
   497   "SURJECTIVE_ON_RIGHT_INVERSE" > "HOLLight.hollight.SURJECTIVE_ON_RIGHT_INVERSE"
   498   "SURJECTIVE_IFF_INJECTIVE_GEN" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE_GEN"
   499   "SURJECTIVE_IFF_INJECTIVE" > "HOLLight.hollight.SURJECTIVE_IFF_INJECTIVE"
   500   "SUPPORT_SUPPORT" > "HOLLight.hollight.SUPPORT_SUPPORT"
   501   "SUPPORT_SUBSET" > "HOLLight.hollight.SUPPORT_SUBSET"
   502   "SUPPORT_EMPTY" > "HOLLight.hollight.SUPPORT_EMPTY"
   503   "SUPPORT_DELTA" > "HOLLight.hollight.SUPPORT_DELTA"
   504   "SUPPORT_CLAUSES" > "HOLLight.hollight.SUPPORT_CLAUSES"
   505   "SUPERADMISSIBLE_T" > "HOLLight.hollight.SUPERADMISSIBLE_T"
   506   "SUPERADMISSIBLE_COND" > "HOLLight.hollight.SUPERADMISSIBLE_COND"
   507   "SUM_UNION_RZERO" > "HOLLight.hollight.SUM_UNION_RZERO"
   508   "SUM_UNION_LZERO" > "HOLLight.hollight.SUM_UNION_LZERO"
   509   "SUM_UNION_EQ" > "HOLLight.hollight.SUM_UNION_EQ"
   510   "SUM_UNION" > "HOLLight.hollight.SUM_UNION"
   511   "SUM_TRIV_NUMSEG" > "HOLLight.hollight.SUM_TRIV_NUMSEG"
   512   "SUM_SWAP_NUMSEG" > "HOLLight.hollight.SUM_SWAP_NUMSEG"
   513   "SUM_SWAP" > "HOLLight.hollight.SUM_SWAP"
   514   "SUM_SUPPORT" > "HOLLight.hollight.SUM_SUPPORT"
   515   "SUM_SUPERSET" > "HOLLight.hollight.SUM_SUPERSET"
   516   "SUM_SUM_RESTRICT" > "HOLLight.hollight.SUM_SUM_RESTRICT"
   517   "SUM_SUM_PRODUCT" > "HOLLight.hollight.SUM_SUM_PRODUCT"
   518   "SUM_SUB_NUMSEG" > "HOLLight.hollight.SUM_SUB_NUMSEG"
   519   "SUM_SUBSET_SIMPLE" > "HOLLight.hollight.SUM_SUBSET_SIMPLE"
   520   "SUM_SUBSET" > "HOLLight.hollight.SUM_SUBSET"
   521   "SUM_SUB" > "HOLLight.hollight.SUM_SUB"
   522   "SUM_SING_NUMSEG" > "HOLLight.hollight.SUM_SING_NUMSEG"
   523   "SUM_SING" > "HOLLight.hollight.SUM_SING"
   524   "SUM_RESTRICT_SET" > "HOLLight.hollight.SUM_RESTRICT_SET"
   525   "SUM_RESTRICT" > "HOLLight.hollight.SUM_RESTRICT"
   526   "SUM_POS_LE_NUMSEG" > "HOLLight.hollight.SUM_POS_LE_NUMSEG"
   527   "SUM_POS_LE" > "HOLLight.hollight.SUM_POS_LE"
   528   "SUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_POS_EQ_0_NUMSEG"
   529   "SUM_POS_EQ_0" > "HOLLight.hollight.SUM_POS_EQ_0"
   530   "SUM_POS_BOUND" > "HOLLight.hollight.SUM_POS_BOUND"
   531   "SUM_OFFSET_0" > "HOLLight.hollight.SUM_OFFSET_0"
   532   "SUM_OFFSET" > "HOLLight.hollight.SUM_OFFSET"
   533   "SUM_NEG_NUMSEG" > "HOLLight.hollight.SUM_NEG_NUMSEG"
   534   "SUM_NEG" > "HOLLight.hollight.SUM_NEG"
   535   "SUM_MULTICOUNT_GEN" > "HOLLight.hollight.SUM_MULTICOUNT_GEN"
   536   "SUM_MULTICOUNT" > "HOLLight.hollight.SUM_MULTICOUNT"
   537   "SUM_LT_ALL" > "HOLLight.hollight.SUM_LT_ALL"
   538   "SUM_LT" > "HOLLight.hollight.SUM_LT"
   539   "SUM_LE_NUMSEG" > "HOLLight.hollight.SUM_LE_NUMSEG"
   540   "SUM_LE" > "HOLLight.hollight.SUM_LE"
   541   "SUM_IMAGE_GEN" > "HOLLight.hollight.SUM_IMAGE_GEN"
   542   "SUM_IMAGE" > "HOLLight.hollight.SUM_IMAGE"
   543   "SUM_EQ_SUPERSET" > "HOLLight.hollight.SUM_EQ_SUPERSET"
   544   "SUM_EQ_NUMSEG" > "HOLLight.hollight.SUM_EQ_NUMSEG"
   545   "SUM_EQ_GENERAL" > "HOLLight.hollight.SUM_EQ_GENERAL"
   546   "SUM_EQ_0_NUMSEG" > "HOLLight.hollight.SUM_EQ_0_NUMSEG"
   547   "SUM_EQ_0" > "HOLLight.hollight.SUM_EQ_0"
   548   "SUM_EQ" > "HOLLight.hollight.SUM_EQ"
   549   "SUM_DIFF" > "HOLLight.hollight.SUM_DIFF"
   550   "SUM_DELTA" > "HOLLight.hollight.SUM_DELTA"
   551   "SUM_CONST_NUMSEG" > "HOLLight.hollight.SUM_CONST_NUMSEG"
   552   "SUM_CONST" > "HOLLight.hollight.SUM_CONST"
   553   "SUM_CMUL_NUMSEG" > "HOLLight.hollight.SUM_CMUL_NUMSEG"
   554   "SUM_CMUL" > "HOLLight.hollight.SUM_CMUL"
   555   "SUM_CLAUSES_RIGHT" > "HOLLight.hollight.SUM_CLAUSES_RIGHT"
   556   "SUM_CLAUSES_NUMSEG" > "HOLLight.hollight.SUM_CLAUSES_NUMSEG"
   557   "SUM_CLAUSES_LEFT" > "HOLLight.hollight.SUM_CLAUSES_LEFT"
   558   "SUM_CLAUSES" > "HOLLight.hollight.SUM_CLAUSES"
   559   "SUM_BOUND_LT_GEN" > "HOLLight.hollight.SUM_BOUND_LT_GEN"
   560   "SUM_BOUND_LT_ALL" > "HOLLight.hollight.SUM_BOUND_LT_ALL"
   561   "SUM_BOUND_LT" > "HOLLight.hollight.SUM_BOUND_LT"
   562   "SUM_BOUND_GEN" > "HOLLight.hollight.SUM_BOUND_GEN"
   563   "SUM_BOUND" > "HOLLight.hollight.SUM_BOUND"
   564   "SUM_BIJECTION" > "HOLLight.hollight.SUM_BIJECTION"
   565   "SUM_ADD_SPLIT" > "HOLLight.hollight.SUM_ADD_SPLIT"
   566   "SUM_ADD_NUMSEG" > "HOLLight.hollight.SUM_ADD_NUMSEG"
   567   "SUM_ADD" > "HOLLight.hollight.SUM_ADD"
   568   "SUM_ABS_NUMSEG" > "HOLLight.hollight.SUM_ABS_NUMSEG"
   569   "SUM_ABS_BOUND" > "HOLLight.hollight.SUM_ABS_BOUND"
   570   "SUM_ABS" > "HOLLight.hollight.SUM_ABS"
   571   "SUM_0" > "HOLLight.hollight.SUM_0"
   572   "SUC_SUB1" > "HOLLight.hollight.SUC_SUB1"
   573   "SUC_INJ" > "Nat.nat.simps_3"
   574   "SUB_SUC" > "Nat.diff_Suc_Suc"
   575   "SUB_REFL" > "Nat.diff_self_eq_0"
   576   "SUB_PRESUC" > "HOLLight.hollight.SUB_PRESUC"
   577   "SUB_EQ_0" > "HOLLight.hollight.SUB_EQ_0"
   578   "SUB_ELIM_THM" > "HOLLight.hollight.SUB_ELIM_THM"
   579   "SUB_ADD_RCANCEL" > "Nat.diff_cancel2"
   580   "SUB_ADD_LCANCEL" > "Nat.diff_cancel"
   581   "SUB_ADD" > "HOLLight.hollight.SUB_ADD"
   582   "SUB_0" > "HOLLight.hollight.SUB_0"
   583   "SUBSET_def" > "HOLLight.hollight.SUBSET_def"
   584   "SUBSET_UNIV" > "HOLLight.hollight.SUBSET_UNIV"
   585   "SUBSET_UNION_ABSORPTION" > "HOLLight.hollight.SUBSET_UNION_ABSORPTION"
   586   "SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
   587   "SUBSET_TRANS" > "HOLLight.hollight.SUBSET_TRANS"
   588   "SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
   589   "SUBSET_REFL" > "HOLLight.hollight.SUBSET_REFL"
   590   "SUBSET_PSUBSET_TRANS" > "HOLLight.hollight.SUBSET_PSUBSET_TRANS"
   591   "SUBSET_NUMSEG" > "HOLLight.hollight.SUBSET_NUMSEG"
   592   "SUBSET_INTER_ABSORPTION" > "HOLLight.hollight.SUBSET_INTER_ABSORPTION"
   593   "SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
   594   "SUBSET_INSERT" > "HOLLight.hollight.SUBSET_INSERT"
   595   "SUBSET_IMAGE" > "HOLLight.hollight.SUBSET_IMAGE"
   596   "SUBSET_EMPTY" > "HOLLight.hollight.SUBSET_EMPTY"
   597   "SUBSET_DIFF" > "HOLLight.hollight.SUBSET_DIFF"
   598   "SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
   599   "SUBSET_ANTISYM" > "HOLLight.hollight.SUBSET_ANTISYM"
   600   "SOME_def" > "HOLLight.hollight.SOME_def"
   601   "SNDCART_PASTECART" > "HOLLight.hollight.SNDCART_PASTECART"
   602   "SND" > "Product_Type.snd_conv"
   603   "SKOLEM_THM" > "HOLLight.hollight.SKOLEM_THM"
   604   "SING_def" > "HOLLight.hollight.SING_def"
   605   "SIMPLE_IMAGE" > "HOLLight.hollight.SIMPLE_IMAGE"
   606   "SET_RECURSION_LEMMA" > "HOLLight.hollight.SET_RECURSION_LEMMA"
   607   "SET_OF_LIST_OF_SET" > "HOLLight.hollight.SET_OF_LIST_OF_SET"
   608   "SET_OF_LIST_APPEND" > "HOLLight.hollight.SET_OF_LIST_APPEND"
   609   "SET_CASES" > "HOLLight.hollight.SET_CASES"
   610   "SETSPEC_def" > "HOLLight.hollight.SETSPEC_def"
   611   "SEMIRING_PTHS" > "HOLLight.hollight.SEMIRING_PTHS"
   612   "SELECT_UNIQUE" > "HOLLight.hollight.SELECT_UNIQUE"
   613   "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
   614   "SELECT_LEMMA" > "Hilbert_Choice.some_sym_eq_trivial"
   615   "RIGHT_SUB_DISTRIB" > "Nat.nat_distrib_3"
   616   "RIGHT_OR_FORALL_THM" > "HOL.all_simps_4"
   617   "RIGHT_OR_EXISTS_THM" > "HOL.ex_simps_4"
   618   "RIGHT_OR_DISTRIB" > "HOL.conj_disj_distribR"
   619   "RIGHT_IMP_FORALL_THM" > "HOL.all_simps_6"
   620   "RIGHT_IMP_EXISTS_THM" > "HOL.ex_simps_6"
   621   "RIGHT_FORALL_OR_THM" > "HOL.all_simps_4"
   622   "RIGHT_FORALL_IMP_THM" > "HOL.all_simps_6"
   623   "RIGHT_EXISTS_IMP_THM" > "HOL.ex_simps_6"
   624   "RIGHT_EXISTS_AND_THM" > "HOL.ex_simps_2"
   625   "RIGHT_AND_FORALL_THM" > "HOL.all_simps_2"
   626   "RIGHT_AND_EXISTS_THM" > "HOL.ex_simps_2"
   627   "RIGHT_ADD_DISTRIB" > "Nat.nat_distrib_1"
   628   "REVERSE_def" > "HOLLight.hollight.REVERSE_def"
   629   "REVERSE_REVERSE" > "HOLLight.hollight.REVERSE_REVERSE"
   630   "REVERSE_APPEND" > "HOLLight.hollight.REVERSE_APPEND"
   631   "REST_def" > "HOLLight.hollight.REST_def"
   632   "REP_ABS_PAIR" > "HOLLightCompat.REP_ABS_PAIR"
   633   "REPLICATE_def" > "HOLLight.hollight.REPLICATE_def"
   634   "REFL_CLAUSE" > "HOL.simp_thms_6"
   635   "RECURSION_CASEWISE_PAIRWISE" > "HOLLight.hollight.RECURSION_CASEWISE_PAIRWISE"
   636   "RECURSION_CASEWISE" > "HOLLight.hollight.RECURSION_CASEWISE"
   637   "REAL_WLOG_LT" > "HOLLight.hollight.REAL_WLOG_LT"
   638   "REAL_WLOG_LE" > "HOLLight.hollight.REAL_WLOG_LE"
   639   "REAL_SUB_TRIANGLE" > "HOLLight.hollight.REAL_SUB_TRIANGLE"
   640   "REAL_SUB_SUB2" > "HOLLight.hollight.REAL_SUB_SUB2"
   641   "REAL_SUB_SUB" > "HOLLight.hollight.REAL_SUB_SUB"
   642   "REAL_SUB_RZERO" > "HOLLight.hollight.REAL_SUB_RZERO"
   643   "REAL_SUB_RNEG" > "HOLLight.hollight.REAL_SUB_RNEG"
   644   "REAL_SUB_REFL" > "HOLLight.hollight.REAL_SUB_REFL"
   645   "REAL_SUB_RDISTRIB" > "HOLLight.hollight.REAL_SUB_RDISTRIB"
   646   "REAL_SUB_NEG2" > "HOLLight.hollight.REAL_SUB_NEG2"
   647   "REAL_SUB_LZERO" > "HOLLight.hollight.REAL_SUB_LZERO"
   648   "REAL_SUB_LT" > "HOLLight.hollight.REAL_SUB_LT"
   649   "REAL_SUB_LNEG" > "HOLLight.hollight.REAL_SUB_LNEG"
   650   "REAL_SUB_LE" > "HOLLight.hollight.REAL_SUB_LE"
   651   "REAL_SUB_LDISTRIB" > "HOLLight.hollight.REAL_SUB_LDISTRIB"
   652   "REAL_SUB_INV" > "HOLLight.hollight.REAL_SUB_INV"
   653   "REAL_SUB_ADD2" > "HOLLight.hollight.REAL_SUB_ADD2"
   654   "REAL_SUB_ADD" > "HOLLight.hollight.REAL_SUB_ADD"
   655   "REAL_SUB_ABS" > "HOLLight.hollight.REAL_SUB_ABS"
   656   "REAL_SUB_0" > "HOLLight.hollight.REAL_SUB_0"
   657   "REAL_SOS_EQ_0" > "HOLLight.hollight.REAL_SOS_EQ_0"
   658   "REAL_RNEG_UNIQ" > "HOLLight.hollight.REAL_RNEG_UNIQ"
   659   "REAL_POW_SUB" > "HOLLight.hollight.REAL_POW_SUB"
   660   "REAL_POW_POW" > "HOLLight.hollight.REAL_POW_POW"
   661   "REAL_POW_ONE" > "HOLLight.hollight.REAL_POW_ONE"
   662   "REAL_POW_NZ" > "HOLLight.hollight.REAL_POW_NZ"
   663   "REAL_POW_NEG" > "HOLLight.hollight.REAL_POW_NEG"
   664   "REAL_POW_MUL" > "HOLLight.hollight.REAL_POW_MUL"
   665   "REAL_POW_MONO_LT" > "HOLLight.hollight.REAL_POW_MONO_LT"
   666   "REAL_POW_MONO" > "HOLLight.hollight.REAL_POW_MONO"
   667   "REAL_POW_LT2" > "HOLLight.hollight.REAL_POW_LT2"
   668   "REAL_POW_LT" > "HOLLight.hollight.REAL_POW_LT"
   669   "REAL_POW_LE_1" > "HOLLight.hollight.REAL_POW_LE_1"
   670   "REAL_POW_LE2" > "HOLLight.hollight.REAL_POW_LE2"
   671   "REAL_POW_LE" > "HOLLight.hollight.REAL_POW_LE"
   672   "REAL_POW_INV" > "HOLLight.hollight.REAL_POW_INV"
   673   "REAL_POW_EQ_0" > "HOLLight.hollight.REAL_POW_EQ_0"
   674   "REAL_POW_DIV" > "HOLLight.hollight.REAL_POW_DIV"
   675   "REAL_POW_ADD" > "HOLLight.hollight.REAL_POW_ADD"
   676   "REAL_POW_2" > "HOLLight.hollight.REAL_POW_2"
   677   "REAL_POW_1_LE" > "HOLLight.hollight.REAL_POW_1_LE"
   678   "REAL_POW_1" > "HOLLight.hollight.REAL_POW_1"
   679   "REAL_POW2_ABS" > "HOLLight.hollight.REAL_POW2_ABS"
   680   "REAL_POS_NZ" > "HOLLight.hollight.REAL_POS_NZ"
   681   "REAL_POS" > "HOLLight.hollight.REAL_POS"
   682   "REAL_POLY_NEG_CLAUSES" > "HOLLight.hollight.REAL_POLY_NEG_CLAUSES"
   683   "REAL_POLY_CLAUSES" > "HOLLight.hollight.REAL_POLY_CLAUSES"
   684   "REAL_OF_NUM_SUM_NUMSEG" > "HOLLight.hollight.REAL_OF_NUM_SUM_NUMSEG"
   685   "REAL_OF_NUM_SUM" > "HOLLight.hollight.REAL_OF_NUM_SUM"
   686   "REAL_OF_NUM_SUC" > "HOLLight.hollight.REAL_OF_NUM_SUC"
   687   "REAL_OF_NUM_SUB" > "HOLLight.hollight.REAL_OF_NUM_SUB"
   688   "REAL_OF_NUM_POW" > "HOLLight.hollight.REAL_OF_NUM_POW"
   689   "REAL_OF_NUM_LT" > "HOLLight.hollight.REAL_OF_NUM_LT"
   690   "REAL_OF_NUM_GT" > "HOLLight.hollight.REAL_OF_NUM_GT"
   691   "REAL_OF_NUM_GE" > "HOLLight.hollight.REAL_OF_NUM_GE"
   692   "REAL_NOT_LT" > "HOLLight.hollight.REAL_NOT_LT"
   693   "REAL_NOT_LE" > "HOLLight.hollight.real_lt_def"
   694   "REAL_NOT_EQ" > "HOLLight.hollight.REAL_NOT_EQ"
   695   "REAL_NEG_SUB" > "HOLLight.hollight.REAL_NEG_SUB"
   696   "REAL_NEG_RMUL" > "HOLLight.hollight.REAL_NEG_RMUL"
   697   "REAL_NEG_NEG" > "HOLLight.hollight.REAL_NEG_NEG"
   698   "REAL_NEG_MUL2" > "HOLLight.hollight.REAL_NEG_MUL2"
   699   "REAL_NEG_MINUS1" > "HOLLight.hollight.REAL_NEG_MINUS1"
   700   "REAL_NEG_LT0" > "HOLLight.hollight.REAL_NEG_LT0"
   701   "REAL_NEG_LMUL" > "HOLLight.hollight.REAL_NEG_LMUL"
   702   "REAL_NEG_LE0" > "HOLLight.hollight.REAL_NEG_LE0"
   703   "REAL_NEG_GT0" > "HOLLight.hollight.REAL_NEG_GT0"
   704   "REAL_NEG_GE0" > "HOLLight.hollight.REAL_NEG_GE0"
   705   "REAL_NEG_EQ_0" > "HOLLight.hollight.REAL_NEG_EQ_0"
   706   "REAL_NEG_EQ" > "HOLLight.hollight.REAL_NEG_EQ"
   707   "REAL_NEG_ADD" > "HOLLight.hollight.REAL_NEG_ADD"
   708   "REAL_NEG_0" > "HOLLight.hollight.REAL_NEG_0"
   709   "REAL_NEGNEG" > "HOLLight.hollight.REAL_NEGNEG"
   710   "REAL_MUL_RZERO" > "HOLLight.hollight.REAL_MUL_RZERO"
   711   "REAL_MUL_RNEG" > "HOLLight.hollight.REAL_MUL_RNEG"
   712   "REAL_MUL_RINV_UNIQ" > "HOLLight.hollight.REAL_MUL_RINV_UNIQ"
   713   "REAL_MUL_RINV" > "HOLLight.hollight.REAL_MUL_RINV"
   714   "REAL_MUL_RID" > "HOLLight.hollight.REAL_MUL_RID"
   715   "REAL_MUL_LZERO" > "HOLLight.hollight.REAL_MUL_LZERO"
   716   "REAL_MUL_LNEG" > "HOLLight.hollight.REAL_MUL_LNEG"
   717   "REAL_MUL_LINV_UNIQ" > "HOLLight.hollight.REAL_MUL_LINV_UNIQ"
   718   "REAL_MUL_AC" > "HOLLight.hollight.REAL_MUL_AC"
   719   "REAL_MUL_2" > "HOLLight.hollight.REAL_MUL_2"
   720   "REAL_MIN_SYM" > "HOLLight.hollight.REAL_MIN_SYM"
   721   "REAL_MIN_MIN" > "HOLLight.hollight.REAL_MIN_MIN"
   722   "REAL_MIN_MAX" > "HOLLight.hollight.REAL_MIN_MAX"
   723   "REAL_MIN_LT" > "HOLLight.hollight.REAL_MIN_LT"
   724   "REAL_MIN_LE" > "HOLLight.hollight.REAL_MIN_LE"
   725   "REAL_MIN_ASSOC" > "HOLLight.hollight.REAL_MIN_ASSOC"
   726   "REAL_MIN_ACI" > "HOLLight.hollight.REAL_MIN_ACI"
   727   "REAL_MAX_SYM" > "HOLLight.hollight.REAL_MAX_SYM"
   728   "REAL_MAX_MIN" > "HOLLight.hollight.REAL_MAX_MIN"
   729   "REAL_MAX_MAX" > "HOLLight.hollight.REAL_MAX_MAX"
   730   "REAL_MAX_LT" > "HOLLight.hollight.REAL_MAX_LT"
   731   "REAL_MAX_LE" > "HOLLight.hollight.REAL_MAX_LE"
   732   "REAL_MAX_ASSOC" > "HOLLight.hollight.REAL_MAX_ASSOC"
   733   "REAL_MAX_ACI" > "HOLLight.hollight.REAL_MAX_ACI"
   734   "REAL_LT_TRANS" > "HOLLight.hollight.REAL_LT_TRANS"
   735   "REAL_LT_TOTAL" > "HOLLight.hollight.REAL_LT_TOTAL"
   736   "REAL_LT_SUB_RADD" > "HOLLight.hollight.REAL_LT_SUB_RADD"
   737   "REAL_LT_SUB_LADD" > "HOLLight.hollight.REAL_LT_SUB_LADD"
   738   "REAL_LT_SQUARE" > "HOLLight.hollight.REAL_LT_SQUARE"
   739   "REAL_LT_RNEG" > "HOLLight.hollight.REAL_LT_RNEG"
   740   "REAL_LT_RMUL_EQ" > "HOLLight.hollight.REAL_LT_RMUL_EQ"
   741   "REAL_LT_RMUL" > "HOLLight.hollight.REAL_LT_RMUL"
   742   "REAL_LT_REFL" > "HOLLight.hollight.REAL_LT_REFL"
   743   "REAL_LT_RDIV_EQ" > "HOLLight.hollight.REAL_LT_RDIV_EQ"
   744   "REAL_LT_RCANCEL_IMP" > "HOLLight.hollight.REAL_LT_RCANCEL_IMP"
   745   "REAL_LT_RADD" > "HOLLight.hollight.REAL_LT_RADD"
   746   "REAL_LT_POW2" > "HOLLight.hollight.REAL_LT_POW2"
   747   "REAL_LT_NEGTOTAL" > "HOLLight.hollight.REAL_LT_NEGTOTAL"
   748   "REAL_LT_NEG2" > "HOLLight.hollight.REAL_LT_NEG2"
   749   "REAL_LT_NEG" > "HOLLight.hollight.REAL_LT_NEG"
   750   "REAL_LT_MUL2" > "HOLLight.hollight.REAL_LT_MUL2"
   751   "REAL_LT_MUL" > "HOLLight.hollight.REAL_LT_MUL"
   752   "REAL_LT_MIN" > "HOLLight.hollight.REAL_LT_MIN"
   753   "REAL_LT_MAX" > "HOLLight.hollight.REAL_LT_MAX"
   754   "REAL_LT_LNEG" > "HOLLight.hollight.REAL_LT_LNEG"
   755   "REAL_LT_LMUL_EQ" > "HOLLight.hollight.REAL_LT_LMUL_EQ"
   756   "REAL_LT_LMUL" > "HOLLight.hollight.REAL_LT_LMUL"
   757   "REAL_LT_LE" > "HOLLight.hollight.REAL_LT_LE"
   758   "REAL_LT_LDIV_EQ" > "HOLLight.hollight.REAL_LT_LDIV_EQ"
   759   "REAL_LT_LCANCEL_IMP" > "HOLLight.hollight.REAL_LT_LCANCEL_IMP"
   760   "REAL_LT_LADD_IMP" > "HOLLight.hollight.REAL_LT_LADD_IMP"
   761   "REAL_LT_LADD" > "HOLLight.hollight.REAL_LT_LADD"
   762   "REAL_LT_INV_EQ" > "HOLLight.hollight.REAL_LT_INV_EQ"
   763   "REAL_LT_INV2" > "HOLLight.hollight.REAL_LT_INV2"
   764   "REAL_LT_INV" > "HOLLight.hollight.REAL_LT_INV"
   765   "REAL_LT_IMP_NZ" > "HOLLight.hollight.REAL_LT_IMP_NZ"
   766   "REAL_LT_IMP_NE" > "HOLLight.hollight.REAL_LT_IMP_NE"
   767   "REAL_LT_IMP_LE" > "HOLLight.hollight.REAL_LT_IMP_LE"
   768   "REAL_LT_GT" > "HOLLight.hollight.REAL_LT_GT"
   769   "REAL_LT_DIV2_EQ" > "HOLLight.hollight.REAL_LT_DIV2_EQ"
   770   "REAL_LT_DIV" > "HOLLight.hollight.REAL_LT_DIV"
   771   "REAL_LT_ANTISYM" > "HOLLight.hollight.REAL_LT_ANTISYM"
   772   "REAL_LT_ADD_SUB" > "HOLLight.hollight.REAL_LT_ADD_SUB"
   773   "REAL_LT_ADDR" > "HOLLight.hollight.REAL_LT_ADDR"
   774   "REAL_LT_ADDNEG2" > "HOLLight.hollight.REAL_LT_ADDNEG2"
   775   "REAL_LT_ADDNEG" > "HOLLight.hollight.REAL_LT_ADDNEG"
   776   "REAL_LT_ADDL" > "HOLLight.hollight.REAL_LT_ADDL"
   777   "REAL_LT_ADD2" > "HOLLight.hollight.REAL_LT_ADD2"
   778   "REAL_LT_ADD1" > "HOLLight.hollight.REAL_LT_ADD1"
   779   "REAL_LT_ADD" > "HOLLight.hollight.REAL_LT_ADD"
   780   "REAL_LT_01" > "HOLLight.hollight.REAL_LT_01"
   781   "REAL_LTE_TRANS" > "HOLLight.hollight.REAL_LTE_TRANS"
   782   "REAL_LTE_TOTAL" > "HOLLight.hollight.REAL_LTE_TOTAL"
   783   "REAL_LTE_ANTISYM" > "HOLLight.hollight.REAL_LTE_ANTISYM"
   784   "REAL_LTE_ADD2" > "HOLLight.hollight.REAL_LTE_ADD2"
   785   "REAL_LTE_ADD" > "HOLLight.hollight.REAL_LTE_ADD"
   786   "REAL_LNEG_UNIQ" > "HOLLight.hollight.REAL_LNEG_UNIQ"
   787   "REAL_LE_TOTAL" > "HOLLight.hollight.REAL_LE_TOTAL"
   788   "REAL_LE_SUB_RADD" > "HOLLight.hollight.REAL_LE_SUB_RADD"
   789   "REAL_LE_SUB_LADD" > "HOLLight.hollight.REAL_LE_SUB_LADD"
   790   "REAL_LE_SQUARE_ABS" > "HOLLight.hollight.REAL_LE_SQUARE_ABS"
   791   "REAL_LE_SQUARE" > "HOLLight.hollight.REAL_LE_SQUARE"
   792   "REAL_LE_RNEG" > "HOLLight.hollight.REAL_LE_RNEG"
   793   "REAL_LE_RMUL_EQ" > "HOLLight.hollight.REAL_LE_RMUL_EQ"
   794   "REAL_LE_RMUL" > "HOLLight.hollight.REAL_LE_RMUL"
   795   "REAL_LE_REFL" > "HOLLight.hollight.REAL_LE_REFL"
   796   "REAL_LE_RDIV_EQ" > "HOLLight.hollight.REAL_LE_RDIV_EQ"
   797   "REAL_LE_RCANCEL_IMP" > "HOLLight.hollight.REAL_LE_RCANCEL_IMP"
   798   "REAL_LE_RADD" > "HOLLight.hollight.REAL_LE_RADD"
   799   "REAL_LE_POW2" > "HOLLight.hollight.REAL_LE_POW2"
   800   "REAL_LE_NEGTOTAL" > "HOLLight.hollight.REAL_LE_NEGTOTAL"
   801   "REAL_LE_NEGR" > "HOLLight.hollight.REAL_LE_NEGR"
   802   "REAL_LE_NEGL" > "HOLLight.hollight.REAL_LE_NEGL"
   803   "REAL_LE_NEG2" > "HOLLight.hollight.REAL_LE_NEG2"
   804   "REAL_LE_NEG" > "HOLLight.hollight.REAL_LE_NEG"
   805   "REAL_LE_MUL2" > "HOLLight.hollight.REAL_LE_MUL2"
   806   "REAL_LE_MIN" > "HOLLight.hollight.REAL_LE_MIN"
   807   "REAL_LE_MAX" > "HOLLight.hollight.REAL_LE_MAX"
   808   "REAL_LE_LT" > "HOLLight.hollight.REAL_LE_LT"
   809   "REAL_LE_LNEG" > "HOLLight.hollight.REAL_LE_LNEG"
   810   "REAL_LE_LMUL_EQ" > "HOLLight.hollight.REAL_LE_LMUL_EQ"
   811   "REAL_LE_LMUL" > "HOLLight.hollight.REAL_LE_LMUL"
   812   "REAL_LE_LDIV_EQ" > "HOLLight.hollight.REAL_LE_LDIV_EQ"
   813   "REAL_LE_LCANCEL_IMP" > "HOLLight.hollight.REAL_LE_LCANCEL_IMP"
   814   "REAL_LE_LADD" > "HOLLight.hollight.REAL_LE_LADD"
   815   "REAL_LE_INV_EQ" > "HOLLight.hollight.REAL_LE_INV_EQ"
   816   "REAL_LE_INV2" > "HOLLight.hollight.REAL_LE_INV2"
   817   "REAL_LE_INV" > "HOLLight.hollight.REAL_LE_INV"
   818   "REAL_LE_DOUBLE" > "HOLLight.hollight.REAL_LE_DOUBLE"
   819   "REAL_LE_DIV2_EQ" > "HOLLight.hollight.REAL_LE_DIV2_EQ"
   820   "REAL_LE_DIV" > "HOLLight.hollight.REAL_LE_DIV"
   821   "REAL_LE_ANTISYM" > "HOLLight.hollight.REAL_LE_ANTISYM"
   822   "REAL_LE_ADDR" > "HOLLight.hollight.REAL_LE_ADDR"
   823   "REAL_LE_ADDL" > "HOLLight.hollight.REAL_LE_ADDL"
   824   "REAL_LE_ADD2" > "HOLLight.hollight.REAL_LE_ADD2"
   825   "REAL_LE_ADD" > "HOLLight.hollight.REAL_LE_ADD"
   826   "REAL_LE_01" > "HOLLight.hollight.REAL_LE_01"
   827   "REAL_LET_TRANS" > "HOLLight.hollight.REAL_LET_TRANS"
   828   "REAL_LET_TOTAL" > "HOLLight.hollight.REAL_LET_TOTAL"
   829   "REAL_LET_ANTISYM" > "HOLLight.hollight.REAL_LET_ANTISYM"
   830   "REAL_LET_ADD2" > "HOLLight.hollight.REAL_LET_ADD2"
   831   "REAL_LET_ADD" > "HOLLight.hollight.REAL_LET_ADD"
   832   "REAL_INV_NEG" > "HOLLight.hollight.REAL_INV_NEG"
   833   "REAL_INV_MUL" > "HOLLight.hollight.REAL_INV_MUL"
   834   "REAL_INV_LE_1" > "HOLLight.hollight.REAL_INV_LE_1"
   835   "REAL_INV_INV" > "HOLLight.hollight.REAL_INV_INV"
   836   "REAL_INV_EQ_0" > "HOLLight.hollight.REAL_INV_EQ_0"
   837   "REAL_INV_DIV" > "HOLLight.hollight.REAL_INV_DIV"
   838   "REAL_INV_1_LE" > "HOLLight.hollight.REAL_INV_1_LE"
   839   "REAL_INV_1" > "HOLLight.hollight.REAL_INV_1"
   840   "REAL_HREAL_LEMMA2" > "HOLLight.hollight.REAL_HREAL_LEMMA2"
   841   "REAL_HREAL_LEMMA1" > "HOLLight.hollight.REAL_HREAL_LEMMA1"
   842   "REAL_EQ_SUB_RADD" > "HOLLight.hollight.REAL_EQ_SUB_RADD"
   843   "REAL_EQ_SUB_LADD" > "HOLLight.hollight.REAL_EQ_SUB_LADD"
   844   "REAL_EQ_RDIV_EQ" > "HOLLight.hollight.REAL_EQ_RDIV_EQ"
   845   "REAL_EQ_RCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_RCANCEL_IMP"
   846   "REAL_EQ_NEG2" > "HOLLight.hollight.REAL_EQ_NEG2"
   847   "REAL_EQ_MUL_RCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_RCANCEL"
   848   "REAL_EQ_MUL_LCANCEL" > "HOLLight.hollight.REAL_EQ_MUL_LCANCEL"
   849   "REAL_EQ_LDIV_EQ" > "HOLLight.hollight.REAL_EQ_LDIV_EQ"
   850   "REAL_EQ_LCANCEL_IMP" > "HOLLight.hollight.REAL_EQ_LCANCEL_IMP"
   851   "REAL_EQ_IMP_LE" > "HOLLight.hollight.REAL_EQ_IMP_LE"
   852   "REAL_EQ_ADD_RCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL_0"
   853   "REAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_RCANCEL"
   854   "REAL_EQ_ADD_LCANCEL_0" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL_0"
   855   "REAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.REAL_EQ_ADD_LCANCEL"
   856   "REAL_ENTIRE" > "HOLLight.hollight.REAL_ENTIRE"
   857   "REAL_DOWN2" > "HOLLight.hollight.REAL_DOWN2"
   858   "REAL_DOWN" > "HOLLight.hollight.REAL_DOWN"
   859   "REAL_DIV_RMUL" > "HOLLight.hollight.REAL_DIV_RMUL"
   860   "REAL_DIV_REFL" > "HOLLight.hollight.REAL_DIV_REFL"
   861   "REAL_DIV_POW2_ALT" > "HOLLight.hollight.REAL_DIV_POW2_ALT"
   862   "REAL_DIV_POW2" > "HOLLight.hollight.REAL_DIV_POW2"
   863   "REAL_DIV_LMUL" > "HOLLight.hollight.REAL_DIV_LMUL"
   864   "REAL_DIV_1" > "HOLLight.hollight.REAL_DIV_1"
   865   "REAL_DIFFSQ" > "HOLLight.hollight.REAL_DIFFSQ"
   866   "REAL_COMPLETE_SOMEPOS" > "HOLLight.hollight.REAL_COMPLETE_SOMEPOS"
   867   "REAL_COMPLETE" > "HOLLight.hollight.REAL_COMPLETE"
   868   "REAL_ADD_SUB2" > "HOLLight.hollight.REAL_ADD_SUB2"
   869   "REAL_ADD_SUB" > "HOLLight.hollight.REAL_ADD_SUB"
   870   "REAL_ADD_RINV" > "HOLLight.hollight.REAL_ADD_RINV"
   871   "REAL_ADD_RID" > "HOLLight.hollight.REAL_ADD_RID"
   872   "REAL_ADD_RDISTRIB" > "HOLLight.hollight.REAL_ADD_RDISTRIB"
   873   "REAL_ADD_AC" > "HOLLight.hollight.REAL_ADD_AC"
   874   "REAL_ADD2_SUB2" > "HOLLight.hollight.REAL_ADD2_SUB2"
   875   "REAL_ABS_ZERO" > "HOLLight.hollight.REAL_ABS_ZERO"
   876   "REAL_ABS_TRIANGLE_LT" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LT"
   877   "REAL_ABS_TRIANGLE_LE" > "HOLLight.hollight.REAL_ABS_TRIANGLE_LE"
   878   "REAL_ABS_TRIANGLE" > "HOLLight.hollight.REAL_ABS_TRIANGLE"
   879   "REAL_ABS_SUB_ABS" > "HOLLight.hollight.REAL_ABS_SUB_ABS"
   880   "REAL_ABS_SUB" > "HOLLight.hollight.REAL_ABS_SUB"
   881   "REAL_ABS_STILLNZ" > "HOLLight.hollight.REAL_ABS_STILLNZ"
   882   "REAL_ABS_SIGN2" > "HOLLight.hollight.REAL_ABS_SIGN2"
   883   "REAL_ABS_SIGN" > "HOLLight.hollight.REAL_ABS_SIGN"
   884   "REAL_ABS_REFL" > "HOLLight.hollight.REAL_ABS_REFL"
   885   "REAL_ABS_POW" > "HOLLight.hollight.REAL_ABS_POW"
   886   "REAL_ABS_POS" > "HOLLight.hollight.REAL_ABS_POS"
   887   "REAL_ABS_NZ" > "HOLLight.hollight.REAL_ABS_NZ"
   888   "REAL_ABS_NUM" > "HOLLight.hollight.REAL_ABS_NUM"
   889   "REAL_ABS_NEG" > "HOLLight.hollight.REAL_ABS_NEG"
   890   "REAL_ABS_MUL" > "HOLLight.hollight.REAL_ABS_MUL"
   891   "REAL_ABS_LE" > "HOLLight.hollight.REAL_ABS_LE"
   892   "REAL_ABS_INV" > "HOLLight.hollight.REAL_ABS_INV"
   893   "REAL_ABS_DIV" > "HOLLight.hollight.REAL_ABS_DIV"
   894   "REAL_ABS_CIRCLE" > "HOLLight.hollight.REAL_ABS_CIRCLE"
   895   "REAL_ABS_CASES" > "HOLLight.hollight.REAL_ABS_CASES"
   896   "REAL_ABS_BOUNDS" > "HOLLight.hollight.REAL_ABS_BOUNDS"
   897   "REAL_ABS_BOUND" > "HOLLight.hollight.REAL_ABS_BOUND"
   898   "REAL_ABS_BETWEEN2" > "HOLLight.hollight.REAL_ABS_BETWEEN2"
   899   "REAL_ABS_BETWEEN1" > "HOLLight.hollight.REAL_ABS_BETWEEN1"
   900   "REAL_ABS_BETWEEN" > "HOLLight.hollight.REAL_ABS_BETWEEN"
   901   "REAL_ABS_ABS" > "HOLLight.hollight.REAL_ABS_ABS"
   902   "REAL_ABS_1" > "HOLLight.hollight.REAL_ABS_1"
   903   "REAL_ABS_0" > "HOLLight.hollight.REAL_ABS_0"
   904   "RAT_LEMMA5" > "HOLLight.hollight.RAT_LEMMA5"
   905   "RAT_LEMMA4" > "HOLLight.hollight.RAT_LEMMA4"
   906   "RAT_LEMMA3" > "HOLLight.hollight.RAT_LEMMA3"
   907   "RAT_LEMMA2" > "HOLLight.hollight.RAT_LEMMA2"
   908   "RAT_LEMMA1" > "HOLLight.hollight.RAT_LEMMA1"
   909   "PSUBSET_def" > "HOLLight.hollight.PSUBSET_def"
   910   "PSUBSET_UNIV" > "HOLLight.hollight.PSUBSET_UNIV"
   911   "PSUBSET_TRANS" > "HOLLight.hollight.PSUBSET_TRANS"
   912   "PSUBSET_SUBSET_TRANS" > "HOLLight.hollight.PSUBSET_SUBSET_TRANS"
   913   "PSUBSET_MEMBER" > "HOLLight.hollight.PSUBSET_MEMBER"
   914   "PSUBSET_IRREFL" > "HOLLight.hollight.PSUBSET_IRREFL"
   915   "PSUBSET_INSERT_SUBSET" > "HOLLight.hollight.PSUBSET_INSERT_SUBSET"
   916   "PRE_ELIM_THM" > "HOLLight.hollight.PRE_ELIM_THM"
   917   "PASTECART_FST_SND" > "HOLLight.hollight.PASTECART_FST_SND"
   918   "PASTECART_EQ" > "HOLLight.hollight.PASTECART_EQ"
   919   "PASSOC_def" > "HOLLight.hollight.PASSOC_def"
   920   "PAIR_SURJECTIVE" > "Datatype.prod.nchotomy"
   921   "PAIR_EXISTS_THM" > "HOLLight.hollight.PAIR_EXISTS_THM"
   922   "PAIR_EQ" > "Datatype.prod.simps_1"
   923   "PAIRWISE_def" > "HOLLight.hollight.PAIRWISE_def"
   924   "PAIR" > "HOL4Compat.PAIR"
   925   "OUTR_def" > "HOLLight.hollight.OUTR_def"
   926   "OUTL_def" > "HOLLight.hollight.OUTL_def"
   927   "OR_EXISTS_THM" > "HOL.ex_disj_distrib"
   928   "OR_CLAUSES" > "HOLLight.hollight.OR_CLAUSES"
   929   "ONE" > "HOLLight.hollight.ONE"
   930   "ODD_def" > "HOLLight.hollight.ODD_def"
   931   "ODD_MULT" > "HOLLight.hollight.ODD_MULT"
   932   "ODD_MOD" > "HOLLight.hollight.ODD_MOD"
   933   "ODD_EXP" > "HOLLight.hollight.ODD_EXP"
   934   "ODD_EXISTS" > "HOLLight.hollight.ODD_EXISTS"
   935   "ODD_DOUBLE" > "HOLLight.hollight.ODD_DOUBLE"
   936   "ODD_ADD" > "HOLLight.hollight.ODD_ADD"
   937   "NUM_INTEGRAL_LEMMA" > "HOLLight.hollight.NUM_INTEGRAL_LEMMA"
   938   "NUM_INTEGRAL" > "HOLLight.hollight.NUM_INTEGRAL"
   939   "NUMSUM_def" > "HOLLight.hollight.NUMSUM_def"
   940   "NUMSUM_INJ" > "HOLLight.hollight.NUMSUM_INJ"
   941   "NUMSND_def" > "HOLLight.hollight.NUMSND_def"
   942   "NUMSEG_SING" > "HOLLight.hollight.NUMSEG_SING"
   943   "NUMSEG_RREC" > "HOLLight.hollight.NUMSEG_RREC"
   944   "NUMSEG_REC" > "HOLLight.hollight.NUMSEG_REC"
   945   "NUMSEG_OFFSET_IMAGE" > "HOLLight.hollight.NUMSEG_OFFSET_IMAGE"
   946   "NUMSEG_LREC" > "HOLLight.hollight.NUMSEG_LREC"
   947   "NUMSEG_EMPTY" > "HOLLight.hollight.NUMSEG_EMPTY"
   948   "NUMSEG_COMBINE_R" > "HOLLight.hollight.NUMSEG_COMBINE_R"
   949   "NUMSEG_COMBINE_L" > "HOLLight.hollight.NUMSEG_COMBINE_L"
   950   "NUMSEG_CLAUSES" > "HOLLight.hollight.NUMSEG_CLAUSES"
   951   "NUMSEG_ADD_SPLIT" > "HOLLight.hollight.NUMSEG_ADD_SPLIT"
   952   "NUMRIGHT_def" > "HOLLight.hollight.NUMRIGHT_def"
   953   "NUMPAIR_def" > "HOLLight.hollight.NUMPAIR_def"
   954   "NUMPAIR_INJ_LEMMA" > "HOLLight.hollight.NUMPAIR_INJ_LEMMA"
   955   "NUMPAIR_INJ" > "HOLLight.hollight.NUMPAIR_INJ"
   956   "NUMLEFT_def" > "HOLLight.hollight.NUMLEFT_def"
   957   "NUMFST_def" > "HOLLight.hollight.NUMFST_def"
   958   "NULL_def" > "HOLLight.hollight.NULL_def"
   959   "NSUM_UNION_RZERO" > "HOLLight.hollight.NSUM_UNION_RZERO"
   960   "NSUM_UNION_LZERO" > "HOLLight.hollight.NSUM_UNION_LZERO"
   961   "NSUM_UNION_EQ" > "HOLLight.hollight.NSUM_UNION_EQ"
   962   "NSUM_UNION" > "HOLLight.hollight.NSUM_UNION"
   963   "NSUM_TRIV_NUMSEG" > "HOLLight.hollight.NSUM_TRIV_NUMSEG"
   964   "NSUM_SWAP_NUMSEG" > "HOLLight.hollight.NSUM_SWAP_NUMSEG"
   965   "NSUM_SWAP" > "HOLLight.hollight.NSUM_SWAP"
   966   "NSUM_SUPPORT" > "HOLLight.hollight.NSUM_SUPPORT"
   967   "NSUM_SUPERSET" > "HOLLight.hollight.NSUM_SUPERSET"
   968   "NSUM_SUBSET_SIMPLE" > "HOLLight.hollight.NSUM_SUBSET_SIMPLE"
   969   "NSUM_SUBSET" > "HOLLight.hollight.NSUM_SUBSET"
   970   "NSUM_SING_NUMSEG" > "HOLLight.hollight.NSUM_SING_NUMSEG"
   971   "NSUM_SING" > "HOLLight.hollight.NSUM_SING"
   972   "NSUM_RESTRICT_SET" > "HOLLight.hollight.NSUM_RESTRICT_SET"
   973   "NSUM_RESTRICT" > "HOLLight.hollight.NSUM_RESTRICT"
   974   "NSUM_POS_LE_NUMSEG" > "HOLLight.hollight.NSUM_POS_LE_NUMSEG"
   975   "NSUM_POS_LE" > "HOLLight.hollight.NSUM_POS_LE"
   976   "NSUM_POS_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_POS_EQ_0_NUMSEG"
   977   "NSUM_POS_EQ_0" > "HOLLight.hollight.NSUM_POS_EQ_0"
   978   "NSUM_POS_BOUND" > "HOLLight.hollight.NSUM_POS_BOUND"
   979   "NSUM_OFFSET_0" > "HOLLight.hollight.NSUM_OFFSET_0"
   980   "NSUM_OFFSET" > "HOLLight.hollight.NSUM_OFFSET"
   981   "NSUM_NSUM_RESTRICT" > "HOLLight.hollight.NSUM_NSUM_RESTRICT"
   982   "NSUM_NSUM_PRODUCT" > "HOLLight.hollight.NSUM_NSUM_PRODUCT"
   983   "NSUM_MULTICOUNT_GEN" > "HOLLight.hollight.NSUM_MULTICOUNT_GEN"
   984   "NSUM_MULTICOUNT" > "HOLLight.hollight.NSUM_MULTICOUNT"
   985   "NSUM_LT_ALL" > "HOLLight.hollight.NSUM_LT_ALL"
   986   "NSUM_LT" > "HOLLight.hollight.NSUM_LT"
   987   "NSUM_LE_NUMSEG" > "HOLLight.hollight.NSUM_LE_NUMSEG"
   988   "NSUM_LE" > "HOLLight.hollight.NSUM_LE"
   989   "NSUM_IMAGE_GEN" > "HOLLight.hollight.NSUM_IMAGE_GEN"
   990   "NSUM_IMAGE" > "HOLLight.hollight.NSUM_IMAGE"
   991   "NSUM_EQ_SUPERSET" > "HOLLight.hollight.NSUM_EQ_SUPERSET"
   992   "NSUM_EQ_NUMSEG" > "HOLLight.hollight.NSUM_EQ_NUMSEG"
   993   "NSUM_EQ_GENERAL" > "HOLLight.hollight.NSUM_EQ_GENERAL"
   994   "NSUM_EQ_0_NUMSEG" > "HOLLight.hollight.NSUM_EQ_0_NUMSEG"
   995   "NSUM_EQ_0" > "HOLLight.hollight.NSUM_EQ_0"
   996   "NSUM_EQ" > "HOLLight.hollight.NSUM_EQ"
   997   "NSUM_DIFF" > "HOLLight.hollight.NSUM_DIFF"
   998   "NSUM_DELTA" > "HOLLight.hollight.NSUM_DELTA"
   999   "NSUM_CONST_NUMSEG" > "HOLLight.hollight.NSUM_CONST_NUMSEG"
  1000   "NSUM_CONST" > "HOLLight.hollight.NSUM_CONST"
  1001   "NSUM_CMUL_NUMSEG" > "HOLLight.hollight.NSUM_CMUL_NUMSEG"
  1002   "NSUM_CMUL" > "HOLLight.hollight.NSUM_CMUL"
  1003   "NSUM_CLAUSES_RIGHT" > "HOLLight.hollight.NSUM_CLAUSES_RIGHT"
  1004   "NSUM_CLAUSES_NUMSEG" > "HOLLight.hollight.NSUM_CLAUSES_NUMSEG"
  1005   "NSUM_CLAUSES_LEFT" > "HOLLight.hollight.NSUM_CLAUSES_LEFT"
  1006   "NSUM_CLAUSES" > "HOLLight.hollight.NSUM_CLAUSES"
  1007   "NSUM_BOUND_LT_GEN" > "HOLLight.hollight.NSUM_BOUND_LT_GEN"
  1008   "NSUM_BOUND_LT_ALL" > "HOLLight.hollight.NSUM_BOUND_LT_ALL"
  1009   "NSUM_BOUND_LT" > "HOLLight.hollight.NSUM_BOUND_LT"
  1010   "NSUM_BOUND_GEN" > "HOLLight.hollight.NSUM_BOUND_GEN"
  1011   "NSUM_BOUND" > "HOLLight.hollight.NSUM_BOUND"
  1012   "NSUM_BIJECTION" > "HOLLight.hollight.NSUM_BIJECTION"
  1013   "NSUM_ADD_SPLIT" > "HOLLight.hollight.NSUM_ADD_SPLIT"
  1014   "NSUM_ADD_NUMSEG" > "HOLLight.hollight.NSUM_ADD_NUMSEG"
  1015   "NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
  1016   "NSUM_0" > "HOLLight.hollight.NSUM_0"
  1017   "NOT_UNIV_PSUBSET" > "HOLLight.hollight.NOT_UNIV_PSUBSET"
  1018   "NOT_SUC" > "Nat.nat.simps_1"
  1019   "NOT_PSUBSET_EMPTY" > "HOLLight.hollight.NOT_PSUBSET_EMPTY"
  1020   "NOT_ODD" > "HOLLight.hollight.NOT_ODD"
  1021   "NOT_LT" > "HOLLight.hollight.NOT_LT"
  1022   "NOT_LE" > "HOLLight.hollight.NOT_LE"
  1023   "NOT_IN_EMPTY" > "HOLLight.hollight.NOT_IN_EMPTY"
  1024   "NOT_INSERT_EMPTY" > "HOLLight.hollight.NOT_INSERT_EMPTY"
  1025   "NOT_FORALL_THM" > "Inductive.basic_monos_15"
  1026   "NOT_EXISTS_THM" > "Inductive.basic_monos_16"
  1027   "NOT_EX" > "HOLLight.hollight.NOT_EX"
  1028   "NOT_EVEN" > "HOLLight.hollight.NOT_EVEN"
  1029   "NOT_EQUAL_SETS" > "HOLLight.hollight.NOT_EQUAL_SETS"
  1030   "NOT_EMPTY_INSERT" > "HOLLight.hollight.NOT_EMPTY_INSERT"
  1031   "NOT_CONS_NIL" > "HOLLight.hollight.NOT_CONS_NIL"
  1032   "NOT_CLAUSES_WEAK" > "HOLLight.hollight.NOT_CLAUSES_WEAK"
  1033   "NOT_ALL" > "HOLLight.hollight.NOT_ALL"
  1034   "NONE_def" > "HOLLight.hollight.NONE_def"
  1035   "NIL_def" > "HOLLight.hollight.NIL_def"
  1036   "NEUTRAL_REAL_MUL" > "HOLLight.hollight.NEUTRAL_REAL_MUL"
  1037   "NEUTRAL_REAL_ADD" > "HOLLight.hollight.NEUTRAL_REAL_ADD"
  1038   "NEUTRAL_MUL" > "HOLLight.hollight.NEUTRAL_MUL"
  1039   "NEUTRAL_ADD" > "HOLLight.hollight.NEUTRAL_ADD"
  1040   "NADD_UBOUND" > "HOLLight.hollight.NADD_UBOUND"
  1041   "NADD_SUC" > "HOLLight.hollight.NADD_SUC"
  1042   "NADD_RDISTRIB" > "HOLLight.hollight.NADD_RDISTRIB"
  1043   "NADD_OF_NUM_WELLDEF" > "HOLLight.hollight.NADD_OF_NUM_WELLDEF"
  1044   "NADD_OF_NUM_MUL" > "HOLLight.hollight.NADD_OF_NUM_MUL"
  1045   "NADD_OF_NUM_LE" > "HOLLight.hollight.NADD_OF_NUM_LE"
  1046   "NADD_OF_NUM_EQ" > "HOLLight.hollight.NADD_OF_NUM_EQ"
  1047   "NADD_OF_NUM_ADD" > "HOLLight.hollight.NADD_OF_NUM_ADD"
  1048   "NADD_OF_NUM" > "HOLLight.hollight.NADD_OF_NUM"
  1049   "NADD_NONZERO" > "HOLLight.hollight.NADD_NONZERO"
  1050   "NADD_MUL_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_MUL_WELLDEF_LEMMA"
  1051   "NADD_MUL_WELLDEF" > "HOLLight.hollight.NADD_MUL_WELLDEF"
  1052   "NADD_MUL_SYM" > "HOLLight.hollight.NADD_MUL_SYM"
  1053   "NADD_MUL_LINV_LEMMA8" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA8"
  1054   "NADD_MUL_LINV_LEMMA7a" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7a"
  1055   "NADD_MUL_LINV_LEMMA7" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA7"
  1056   "NADD_MUL_LINV_LEMMA6" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA6"
  1057   "NADD_MUL_LINV_LEMMA5" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA5"
  1058   "NADD_MUL_LINV_LEMMA4" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA4"
  1059   "NADD_MUL_LINV_LEMMA3" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA3"
  1060   "NADD_MUL_LINV_LEMMA2" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA2"
  1061   "NADD_MUL_LINV_LEMMA1" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA1"
  1062   "NADD_MUL_LINV_LEMMA0" > "HOLLight.hollight.NADD_MUL_LINV_LEMMA0"
  1063   "NADD_MUL_LINV" > "HOLLight.hollight.NADD_MUL_LINV"
  1064   "NADD_MUL_LID" > "HOLLight.hollight.NADD_MUL_LID"
  1065   "NADD_MUL_ASSOC" > "HOLLight.hollight.NADD_MUL_ASSOC"
  1066   "NADD_MULTIPLICATIVE" > "HOLLight.hollight.NADD_MULTIPLICATIVE"
  1067   "NADD_MUL" > "HOLLight.hollight.NADD_MUL"
  1068   "NADD_LE_WELLDEF_LEMMA" > "HOLLight.hollight.NADD_LE_WELLDEF_LEMMA"
  1069   "NADD_LE_WELLDEF" > "HOLLight.hollight.NADD_LE_WELLDEF"
  1070   "NADD_LE_TRANS" > "HOLLight.hollight.NADD_LE_TRANS"
  1071   "NADD_LE_TOTAL_LEMMA" > "HOLLight.hollight.NADD_LE_TOTAL_LEMMA"
  1072   "NADD_LE_TOTAL" > "HOLLight.hollight.NADD_LE_TOTAL"
  1073   "NADD_LE_RMUL" > "HOLLight.hollight.NADD_LE_RMUL"
  1074   "NADD_LE_REFL" > "HOLLight.hollight.NADD_LE_REFL"
  1075   "NADD_LE_RADD" > "HOLLight.hollight.NADD_LE_RADD"
  1076   "NADD_LE_LMUL" > "HOLLight.hollight.NADD_LE_LMUL"
  1077   "NADD_LE_LADD" > "HOLLight.hollight.NADD_LE_LADD"
  1078   "NADD_LE_EXISTS" > "HOLLight.hollight.NADD_LE_EXISTS"
  1079   "NADD_LE_ANTISYM" > "HOLLight.hollight.NADD_LE_ANTISYM"
  1080   "NADD_LE_ADD" > "HOLLight.hollight.NADD_LE_ADD"
  1081   "NADD_LE_0" > "HOLLight.hollight.NADD_LE_0"
  1082   "NADD_LDISTRIB" > "HOLLight.hollight.NADD_LDISTRIB"
  1083   "NADD_LBOUND" > "HOLLight.hollight.NADD_LBOUND"
  1084   "NADD_INV_WELLDEF" > "HOLLight.hollight.NADD_INV_WELLDEF"
  1085   "NADD_INV_0" > "HOLLight.hollight.NADD_INV_0"
  1086   "NADD_INV" > "HOLLight.hollight.NADD_INV"
  1087   "NADD_EQ_TRANS" > "HOLLight.hollight.NADD_EQ_TRANS"
  1088   "NADD_EQ_SYM" > "HOLLight.hollight.NADD_EQ_SYM"
  1089   "NADD_EQ_REFL" > "HOLLight.hollight.NADD_EQ_REFL"
  1090   "NADD_EQ_IMP_LE" > "HOLLight.hollight.NADD_EQ_IMP_LE"
  1091   "NADD_DIST_LEMMA" > "HOLLight.hollight.NADD_DIST_LEMMA"
  1092   "NADD_DIST" > "HOLLight.hollight.NADD_DIST"
  1093   "NADD_COMPLETE" > "HOLLight.hollight.NADD_COMPLETE"
  1094   "NADD_CAUCHY" > "HOLLight.hollight.NADD_CAUCHY"
  1095   "NADD_BOUND" > "HOLLight.hollight.NADD_BOUND"
  1096   "NADD_ARCH_ZERO" > "HOLLight.hollight.NADD_ARCH_ZERO"
  1097   "NADD_ARCH_MULT" > "HOLLight.hollight.NADD_ARCH_MULT"
  1098   "NADD_ARCH_LEMMA" > "HOLLight.hollight.NADD_ARCH_LEMMA"
  1099   "NADD_ARCH" > "HOLLight.hollight.NADD_ARCH"
  1100   "NADD_ALTMUL" > "HOLLight.hollight.NADD_ALTMUL"
  1101   "NADD_ADD_WELLDEF" > "HOLLight.hollight.NADD_ADD_WELLDEF"
  1102   "NADD_ADD_SYM" > "HOLLight.hollight.NADD_ADD_SYM"
  1103   "NADD_ADD_LID" > "HOLLight.hollight.NADD_ADD_LID"
  1104   "NADD_ADD_LCANCEL" > "HOLLight.hollight.NADD_ADD_LCANCEL"
  1105   "NADD_ADD_ASSOC" > "HOLLight.hollight.NADD_ADD_ASSOC"
  1106   "NADD_ADDITIVE" > "HOLLight.hollight.NADD_ADDITIVE"
  1107   "NADD_ADD" > "HOLLight.hollight.NADD_ADD"
  1108   "MULT_SYM" > "Int.zmult_ac_2"
  1109   "MULT_SUC" > "Nat.mult_Suc_right"
  1110   "MULT_EXP" > "HOLLight.hollight.MULT_EXP"
  1111   "MULT_EQ_1" > "HOLLight.hollight.MULT_EQ_1"
  1112   "MULT_EQ_0" > "Nat.mult_is_0"
  1113   "MULT_CLAUSES" > "HOLLight.hollight.MULT_CLAUSES"
  1114   "MULT_ASSOC" > "Int.zmult_ac_1"
  1115   "MULT_AC" > "HOLLight.hollight.MULT_AC"
  1116   "MULT_2" > "HOLLight.hollight.MULT_2"
  1117   "MULT_0" > "Nat.mult_0_right"
  1118   "MONO_FORALL" > "Inductive.basic_monos_6"
  1119   "MONO_EXISTS" > "Inductive.basic_monos_5"
  1120   "MONO_COND" > "HOLLight.hollight.MONO_COND"
  1121   "MONO_ALL2" > "HOLLight.hollight.MONO_ALL2"
  1122   "MONO_ALL" > "HOLLight.hollight.MONO_ALL"
  1123   "MONOIDAL_REAL_MUL" > "HOLLight.hollight.MONOIDAL_REAL_MUL"
  1124   "MONOIDAL_REAL_ADD" > "HOLLight.hollight.MONOIDAL_REAL_ADD"
  1125   "MONOIDAL_MUL" > "HOLLight.hollight.MONOIDAL_MUL"
  1126   "MONOIDAL_ADD" > "HOLLight.hollight.MONOIDAL_ADD"
  1127   "MOD_def" > "HOLLight.hollight.MOD_def"
  1128   "MOD_UNIQ" > "HOLLight.hollight.MOD_UNIQ"
  1129   "MOD_MULT_RMOD" > "HOLLight.hollight.MOD_MULT_RMOD"
  1130   "MOD_MULT_MOD2" > "HOLLight.hollight.MOD_MULT_MOD2"
  1131   "MOD_MULT_LMOD" > "HOLLight.hollight.MOD_MULT_LMOD"
  1132   "MOD_MULT_ADD" > "HOLLight.hollight.MOD_MULT_ADD"
  1133   "MOD_MULT2" > "HOLLight.hollight.MOD_MULT2"
  1134   "MOD_MULT" > "HOLLight.hollight.MOD_MULT"
  1135   "MOD_MOD_REFL" > "HOLLight.hollight.MOD_MOD_REFL"
  1136   "MOD_MOD" > "HOLLight.hollight.MOD_MOD"
  1137   "MOD_LT" > "HOLLight.hollight.MOD_LT"
  1138   "MOD_LE" > "HOLLight.hollight.MOD_LE"
  1139   "MOD_EXP_MOD" > "HOLLight.hollight.MOD_EXP_MOD"
  1140   "MOD_EXISTS" > "HOLLight.hollight.MOD_EXISTS"
  1141   "MOD_EQ_0" > "HOLLight.hollight.MOD_EQ_0"
  1142   "MOD_EQ" > "HOLLight.hollight.MOD_EQ"
  1143   "MOD_ADD_MOD" > "HOLLight.hollight.MOD_ADD_MOD"
  1144   "MOD_1" > "HOLLight.hollight.MOD_1"
  1145   "MOD_0" > "HOLLight.hollight.MOD_0"
  1146   "MK_REC_INJ" > "HOLLight.hollight.MK_REC_INJ"
  1147   "MINIMAL" > "HOLLight.hollight.MINIMAL"
  1148   "MEM_def" > "HOLLight.hollight.MEM_def"
  1149   "MEM_MAP" > "HOLLight.hollight.MEM_MAP"
  1150   "MEM_LIST_OF_SET" > "HOLLight.hollight.MEM_LIST_OF_SET"
  1151   "MEM_FILTER" > "HOLLight.hollight.MEM_FILTER"
  1152   "MEM_EL" > "HOLLight.hollight.MEM_EL"
  1153   "MEM_ASSOC" > "HOLLight.hollight.MEM_ASSOC"
  1154   "MEM_APPEND" > "HOLLight.hollight.MEM_APPEND"
  1155   "MEMBER_NOT_EMPTY" > "HOLLight.hollight.MEMBER_NOT_EMPTY"
  1156   "MEASURE_LE" > "HOLLight.hollight.MEASURE_LE"
  1157   "MAP_o" > "HOLLight.hollight.MAP_o"
  1158   "MAP_def" > "HOLLight.hollight.MAP_def"
  1159   "MAP_SND_ZIP" > "HOLLight.hollight.MAP_SND_ZIP"
  1160   "MAP_FST_ZIP" > "HOLLight.hollight.MAP_FST_ZIP"
  1161   "MAP_EQ_DEGEN" > "HOLLight.hollight.MAP_EQ_DEGEN"
  1162   "MAP_EQ_ALL2" > "HOLLight.hollight.MAP_EQ_ALL2"
  1163   "MAP_EQ" > "HOLLight.hollight.MAP_EQ"
  1164   "MAP_APPEND" > "HOLLight.hollight.MAP_APPEND"
  1165   "MAP2_def" > "HOLLight.hollight.MAP2_def"
  1166   "MAP2" > "HOLLight.hollight.MAP2"
  1167   "LT_TRANS" > "HOLLight.hollight.LT_TRANS"
  1168   "LT_SUC_LE" > "HOLLight.hollight.LT_SUC_LE"
  1169   "LT_SUC" > "HOLLight.hollight.LT_SUC"
  1170   "LT_REFL" > "HOLLight.hollight.LT_REFL"
  1171   "LT_NZ" > "HOLLight.hollight.LT_NZ"
  1172   "LT_MULT_RCANCEL" > "HOLLight.hollight.LT_MULT_RCANCEL"
  1173   "LT_MULT_LCANCEL" > "HOLLight.hollight.LT_MULT_LCANCEL"
  1174   "LT_MULT2" > "HOLLight.hollight.LT_MULT2"
  1175   "LT_MULT" > "HOLLight.hollight.LT_MULT"
  1176   "LT_LMULT" > "HOLLight.hollight.LT_LMULT"
  1177   "LT_LE" > "HOLLight.hollight.LT_LE"
  1178   "LT_IMP_LE" > "HOLLight.hollight.LT_IMP_LE"
  1179   "LT_EXP" > "HOLLight.hollight.LT_EXP"
  1180   "LT_EXISTS" > "HOLLight.hollight.LT_EXISTS"
  1181   "LT_CASES" > "HOLLight.hollight.LT_CASES"
  1182   "LT_ANTISYM" > "HOLLight.hollight.LT_ANTISYM"
  1183   "LT_ADD_RCANCEL" > "HOLLight.hollight.LT_ADD_RCANCEL"
  1184   "LT_ADD_LCANCEL" > "HOLLight.hollight.LT_ADD_LCANCEL"
  1185   "LT_ADDR" > "HOLLight.hollight.LT_ADDR"
  1186   "LT_ADD2" > "HOLLight.hollight.LT_ADD2"
  1187   "LT_ADD" > "HOLLight.hollight.LT_ADD"
  1188   "LT_0" > "HOLLight.hollight.LT_0"
  1189   "LTE_TRANS" > "HOLLight.hollight.LTE_TRANS"
  1190   "LTE_CASES" > "HOLLight.hollight.LTE_CASES"
  1191   "LTE_ANTISYM" > "HOLLight.hollight.LTE_ANTISYM"
  1192   "LTE_ADD2" > "HOLLight.hollight.LTE_ADD2"
  1193   "LIST_OF_SET_PROPERTIES" > "HOLLight.hollight.LIST_OF_SET_PROPERTIES"
  1194   "LE_TRANS" > "HOLLight.hollight.LE_TRANS"
  1195   "LE_SUC_LT" > "HOLLight.hollight.LE_SUC_LT"
  1196   "LE_SUC" > "HOLLight.hollight.LE_SUC"
  1197   "LE_SQUARE_REFL" > "HOLLight.hollight.LE_SQUARE_REFL"
  1198   "LE_REFL" > "HOLLight.hollight.LE_REFL"
  1199   "LE_RDIV_EQ" > "HOLLight.hollight.LE_RDIV_EQ"
  1200   "LE_MULT_RCANCEL" > "HOLLight.hollight.LE_MULT_RCANCEL"
  1201   "LE_MULT_LCANCEL" > "HOLLight.hollight.LE_MULT_LCANCEL"
  1202   "LE_MULT2" > "HOLLight.hollight.LE_MULT2"
  1203   "LE_LT" > "HOLLight.hollight.LE_LT"
  1204   "LE_LDIV_EQ" > "HOLLight.hollight.LE_LDIV_EQ"
  1205   "LE_LDIV" > "HOLLight.hollight.LE_LDIV"
  1206   "LE_EXP" > "HOLLight.hollight.LE_EXP"
  1207   "LE_EXISTS" > "HOLLight.hollight.LE_EXISTS"
  1208   "LE_CASES" > "HOLLight.hollight.LE_CASES"
  1209   "LE_ANTISYM" > "HOLLight.hollight.LE_ANTISYM"
  1210   "LE_ADD_RCANCEL" > "HOLLight.hollight.LE_ADD_RCANCEL"
  1211   "LE_ADD_LCANCEL" > "HOLLight.hollight.LE_ADD_LCANCEL"
  1212   "LE_ADDR" > "HOLLight.hollight.LE_ADDR"
  1213   "LE_ADD2" > "HOLLight.hollight.LE_ADD2"
  1214   "LE_ADD" > "HOLLight.hollight.LE_ADD"
  1215   "LE_0" > "HOLLight.hollight.LE_0"
  1216   "LET_TRANS" > "HOLLight.hollight.LET_TRANS"
  1217   "LET_END_def" > "HOLLight.hollight.LET_END_def"
  1218   "LET_CASES" > "HOLLight.hollight.LET_CASES"
  1219   "LET_ANTISYM" > "HOLLight.hollight.LET_ANTISYM"
  1220   "LET_ADD2" > "HOLLight.hollight.LET_ADD2"
  1221   "LENGTH_def" > "HOLLight.hollight.LENGTH_def"
  1222   "LENGTH_REPLICATE" > "HOLLight.hollight.LENGTH_REPLICATE"
  1223   "LENGTH_MAP2" > "HOLLight.hollight.LENGTH_MAP2"
  1224   "LENGTH_MAP" > "HOLLight.hollight.LENGTH_MAP"
  1225   "LENGTH_LIST_OF_SET" > "HOLLight.hollight.LENGTH_LIST_OF_SET"
  1226   "LENGTH_EQ_NIL" > "HOLLight.hollight.LENGTH_EQ_NIL"
  1227   "LENGTH_EQ_CONS" > "HOLLight.hollight.LENGTH_EQ_CONS"
  1228   "LENGTH_APPEND" > "HOLLight.hollight.LENGTH_APPEND"
  1229   "LEFT_SUB_DISTRIB" > "Nat.nat_distrib_4"
  1230   "LEFT_OR_FORALL_THM" > "HOL.all_simps_3"
  1231   "LEFT_OR_EXISTS_THM" > "HOL.ex_simps_3"
  1232   "LEFT_OR_DISTRIB" > "HOL.conj_disj_distribL"
  1233   "LEFT_IMP_FORALL_THM" > "HOL.imp_all"
  1234   "LEFT_IMP_EXISTS_THM" > "HOL.imp_ex"
  1235   "LEFT_FORALL_OR_THM" > "HOL.all_simps_3"
  1236   "LEFT_FORALL_IMP_THM" > "HOL.imp_ex"
  1237   "LEFT_EXISTS_IMP_THM" > "HOL.imp_all"
  1238   "LEFT_EXISTS_AND_THM" > "HOL.ex_simps_1"
  1239   "LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
  1240   "LEFT_AND_EXISTS_THM" > "HOL.ex_simps_1"
  1241   "LEFT_ADD_DISTRIB" > "Nat.nat_distrib_2"
  1242   "LAST_def" > "HOLLight.hollight.LAST_def"
  1243   "LAST_CLAUSES" > "HOLLight.hollight.LAST_CLAUSES"
  1244   "LAMBDA_UNIQUE" > "HOLLight.hollight.LAMBDA_UNIQUE"
  1245   "LAMBDA_ETA" > "HOLLight.hollight.LAMBDA_ETA"
  1246   "LAMBDA_BETA" > "HOLLight.hollight.LAMBDA_BETA"
  1247   "I_THM" > "Fun.id_apply"
  1248   "I_O_ID" > "HOLLight.hollight.I_O_ID"
  1249   "ITSET_def" > "HOLLight.hollight.ITSET_def"
  1250   "ITSET_EQ" > "HOLLight.hollight.ITSET_EQ"
  1251   "ITLIST_def" > "HOLLight.hollight.ITLIST_def"
  1252   "ITLIST_EXTRA" > "HOLLight.hollight.ITLIST_EXTRA"
  1253   "ITLIST2_def" > "HOLLight.hollight.ITLIST2_def"
  1254   "ITLIST2" > "HOLLight.hollight.ITLIST2"
  1255   "ITERATE_UNION_GEN" > "HOLLight.hollight.ITERATE_UNION_GEN"
  1256   "ITERATE_UNION" > "HOLLight.hollight.ITERATE_UNION"
  1257   "ITERATE_SUPPORT" > "HOLLight.hollight.ITERATE_SUPPORT"
  1258   "ITERATE_SING" > "HOLLight.hollight.ITERATE_SING"
  1259   "ITERATE_RELATED" > "HOLLight.hollight.ITERATE_RELATED"
  1260   "ITERATE_ITERATE_PRODUCT" > "HOLLight.hollight.ITERATE_ITERATE_PRODUCT"
  1261   "ITERATE_IMAGE" > "HOLLight.hollight.ITERATE_IMAGE"
  1262   "ITERATE_EQ_NEUTRAL" > "HOLLight.hollight.ITERATE_EQ_NEUTRAL"
  1263   "ITERATE_EQ_GENERAL" > "HOLLight.hollight.ITERATE_EQ_GENERAL"
  1264   "ITERATE_EQ" > "HOLLight.hollight.ITERATE_EQ"
  1265   "ITERATE_DIFF_GEN" > "HOLLight.hollight.ITERATE_DIFF_GEN"
  1266   "ITERATE_DIFF" > "HOLLight.hollight.ITERATE_DIFF"
  1267   "ITERATE_DELTA" > "HOLLight.hollight.ITERATE_DELTA"
  1268   "ITERATE_CLOSED_GEN" > "HOLLight.hollight.ITERATE_CLOSED_GEN"
  1269   "ITERATE_CLOSED" > "HOLLight.hollight.ITERATE_CLOSED"
  1270   "ITERATE_CLAUSES_GEN" > "HOLLight.hollight.ITERATE_CLAUSES_GEN"
  1271   "ITERATE_CLAUSES" > "HOLLight.hollight.ITERATE_CLAUSES"
  1272   "ITERATE_BIJECTION" > "HOLLight.hollight.ITERATE_BIJECTION"
  1273   "ISO_def" > "HOLLight.hollight.ISO_def"
  1274   "ISO_USAGE" > "HOLLight.hollight.ISO_USAGE"
  1275   "ISO_REFL" > "HOLLight.hollight.ISO_REFL"
  1276   "ISO_FUN" > "HOLLight.hollight.ISO_FUN"
  1277   "IN_def" > "HOLLight.hollight.IN_def"
  1278   "IN_UNIV" > "HOLLight.hollight.IN_UNIV"
  1279   "IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
  1280   "IN_UNION" > "HOLLight.hollight.IN_UNION"
  1281   "IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
  1282   "IN_SING" > "HOLLight.hollight.IN_SING"
  1283   "IN_SET_OF_LIST" > "HOLLight.hollight.IN_SET_OF_LIST"
  1284   "IN_REST" > "HOLLight.hollight.IN_REST"
  1285   "IN_NUMSEG" > "HOLLight.hollight.IN_NUMSEG"
  1286   "IN_INTERS" > "HOLLight.hollight.IN_INTERS"
  1287   "IN_INTER" > "HOLLight.hollight.IN_INTER"
  1288   "IN_INSERT" > "HOLLight.hollight.IN_INSERT"
  1289   "IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
  1290   "IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
  1291   "IN_ELIM_PAIR_THM" > "HOLLight.hollight.IN_ELIM_PAIR_THM"
  1292   "IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
  1293   "IN_DIFF" > "HOLLight.hollight.IN_DIFF"
  1294   "IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
  1295   "IN_DELETE" > "HOLLight.hollight.IN_DELETE"
  1296   "INT_POW" > "HOLLight.hollight.INT_POW"
  1297   "INT_LT_DISCRETE" > "HOLLight.hollight.INT_LT_DISCRETE"
  1298   "INT_LT" > "HOLLight.hollight.INT_LT"
  1299   "INT_IMAGE" > "HOLLight.hollight.INT_IMAGE"
  1300   "INT_GT_DISCRETE" > "HOLLight.hollight.INT_GT_DISCRETE"
  1301   "INT_GT" > "HOLLight.hollight.INT_GT"
  1302   "INT_GE" > "HOLLight.hollight.INT_GE"
  1303   "INT_FORALL_POS" > "HOLLight.hollight.INT_FORALL_POS"
  1304   "INT_ARCH" > "HOLLight.hollight.INT_ARCH"
  1305   "INT_ABS_MUL_1" > "HOLLight.hollight.INT_ABS_MUL_1"
  1306   "INT_ABS" > "HOLLight.hollight.INT_ABS"
  1307   "INTER_def" > "HOLLight.hollight.INTER_def"
  1308   "INTER_UNIV" > "HOLLight.hollight.INTER_UNIV"
  1309   "INTER_SUBSET" > "HOLLight.hollight.INTER_SUBSET"
  1310   "INTER_OVER_UNION" > "HOLLight.hollight.INTER_OVER_UNION"
  1311   "INTER_IDEMPOT" > "HOLLight.hollight.INTER_IDEMPOT"
  1312   "INTER_EMPTY" > "HOLLight.hollight.INTER_EMPTY"
  1313   "INTER_COMM" > "HOLLight.hollight.INTER_COMM"
  1314   "INTER_ASSOC" > "HOLLight.hollight.INTER_ASSOC"
  1315   "INTER_ACI" > "HOLLight.hollight.INTER_ACI"
  1316   "INTERS_def" > "HOLLight.hollight.INTERS_def"
  1317   "INTERS_INSERT" > "HOLLight.hollight.INTERS_INSERT"
  1318   "INTERS_2" > "HOLLight.hollight.INTERS_2"
  1319   "INTERS_1" > "HOLLight.hollight.INTERS_1"
  1320   "INTERS_0" > "HOLLight.hollight.INTERS_0"
  1321   "INSERT_def" > "HOLLight.hollight.INSERT_def"
  1322   "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
  1323   "INSERT_UNION_EQ" > "HOLLight.hollight.INSERT_UNION_EQ"
  1324   "INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
  1325   "INSERT_SUBSET" > "HOLLight.hollight.INSERT_SUBSET"
  1326   "INSERT_INTER" > "HOLLight.hollight.INSERT_INTER"
  1327   "INSERT_INSERT" > "HOLLight.hollight.INSERT_INSERT"
  1328   "INSERT_DIFF" > "HOLLight.hollight.INSERT_DIFF"
  1329   "INSERT_DELETE" > "HOLLight.hollight.INSERT_DELETE"
  1330   "INSERT_COMM" > "HOLLight.hollight.INSERT_COMM"
  1331   "INSERT_AC" > "HOLLight.hollight.INSERT_AC"
  1332   "INSERT" > "HOLLight.hollight.INSERT"
  1333   "INJ_def" > "HOLLight.hollight.INJ_def"
  1334   "INJ_INVERSE2" > "HOLLight.hollight.INJ_INVERSE2"
  1335   "INJP_def" > "HOLLight.hollight.INJP_def"
  1336   "INJP_INJ" > "HOLLight.hollight.INJP_INJ"
  1337   "INJN_def" > "HOLLight.hollight.INJN_def"
  1338   "INJN_INJ" > "HOLLight.hollight.INJN_INJ"
  1339   "INJF_def" > "HOLLight.hollight.INJF_def"
  1340   "INJF_INJ" > "HOLLight.hollight.INJF_INJ"
  1341   "INJECTIVE_ON_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_ON_LEFT_INVERSE"
  1342   "INJECTIVE_LEFT_INVERSE" > "HOLLight.hollight.INJECTIVE_LEFT_INVERSE"
  1343   "INJA_def" > "HOLLight.hollight.INJA_def"
  1344   "INJA_INJ" > "HOLLight.hollight.INJA_INJ"
  1345   "INFINITE_def" > "HOLLight.hollight.INFINITE_def"
  1346   "INFINITE_NONEMPTY" > "HOLLight.hollight.INFINITE_NONEMPTY"
  1347   "INFINITE_IMAGE_INJ" > "HOLLight.hollight.INFINITE_IMAGE_INJ"
  1348   "INFINITE_DIFF_FINITE" > "HOLLight.hollight.INFINITE_DIFF_FINITE"
  1349   "IMP_EQ_CLAUSE" > "HOLLight.hollight.IMP_EQ_CLAUSE"
  1350   "IMP_CONJ" > "HOL.imp_conjL"
  1351   "IMP_CLAUSES" > "HOLLight.hollight.IMP_CLAUSES"
  1352   "IMAGE_o" > "HOLLight.hollight.IMAGE_o"
  1353   "IMAGE_def" > "HOLLight.hollight.IMAGE_def"
  1354   "IMAGE_UNION" > "HOLLight.hollight.IMAGE_UNION"
  1355   "IMAGE_SUBSET" > "HOLLight.hollight.IMAGE_SUBSET"
  1356   "IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
  1357   "IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
  1358   "IMAGE_EQ_EMPTY" > "HOLLight.hollight.IMAGE_EQ_EMPTY"
  1359   "IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
  1360   "IMAGE_DELETE_INJ" > "HOLLight.hollight.IMAGE_DELETE_INJ"
  1361   "IMAGE_CONST" > "HOLLight.hollight.IMAGE_CONST"
  1362   "IMAGE_CLAUSES" > "HOLLight.hollight.IMAGE_CLAUSES"
  1363   "HREAL_MUL_RZERO" > "HOLLight.hollight.HREAL_MUL_RZERO"
  1364   "HREAL_MUL_LZERO" > "HOLLight.hollight.HREAL_MUL_LZERO"
  1365   "HREAL_LE_MUL_RCANCEL_IMP" > "HOLLight.hollight.HREAL_LE_MUL_RCANCEL_IMP"
  1366   "HREAL_LE_EXISTS_DEF" > "HOLLight.hollight.HREAL_LE_EXISTS_DEF"
  1367   "HREAL_LE_ADD_RCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_RCANCEL"
  1368   "HREAL_LE_ADD_LCANCEL" > "HOLLight.hollight.HREAL_LE_ADD_LCANCEL"
  1369   "HREAL_LE_ADD2" > "HOLLight.hollight.HREAL_LE_ADD2"
  1370   "HREAL_EQ_ADD_RCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_RCANCEL"
  1371   "HREAL_EQ_ADD_LCANCEL" > "HOLLight.hollight.HREAL_EQ_ADD_LCANCEL"
  1372   "HREAL_ADD_RID" > "HOLLight.hollight.HREAL_ADD_RID"
  1373   "HREAL_ADD_RDISTRIB" > "HOLLight.hollight.HREAL_ADD_RDISTRIB"
  1374   "HREAL_ADD_AC" > "HOLLight.hollight.HREAL_ADD_AC"
  1375   "HD_def" > "HOLLight.hollight.HD_def"
  1376   "HAS_SIZE_def" > "HOLLight.hollight.HAS_SIZE_def"
  1377   "HAS_SIZE_UNIONS" > "HOLLight.hollight.HAS_SIZE_UNIONS"
  1378   "HAS_SIZE_UNION" > "HOLLight.hollight.HAS_SIZE_UNION"
  1379   "HAS_SIZE_SUC" > "HOLLight.hollight.HAS_SIZE_SUC"
  1380   "HAS_SIZE_PRODUCT_DEPENDENT" > "HOLLight.hollight.HAS_SIZE_PRODUCT_DEPENDENT"
  1381   "HAS_SIZE_PRODUCT" > "HOLLight.hollight.HAS_SIZE_PRODUCT"
  1382   "HAS_SIZE_POWERSET" > "HOLLight.hollight.HAS_SIZE_POWERSET"
  1383   "HAS_SIZE_NUMSEG_LT" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LT"
  1384   "HAS_SIZE_NUMSEG_LE" > "HOLLight.hollight.HAS_SIZE_NUMSEG_LE"
  1385   "HAS_SIZE_NUMSEG_1" > "HOLLight.hollight.HAS_SIZE_NUMSEG_1"
  1386   "HAS_SIZE_NUMSEG" > "HOLLight.hollight.HAS_SIZE_NUMSEG"
  1387   "HAS_SIZE_INDEX" > "HOLLight.hollight.HAS_SIZE_INDEX"
  1388   "HAS_SIZE_IMAGE_INJ" > "HOLLight.hollight.HAS_SIZE_IMAGE_INJ"
  1389   "HAS_SIZE_FUNSPACE" > "HOLLight.hollight.HAS_SIZE_FUNSPACE"
  1390   "HAS_SIZE_FINITE_IMAGE" > "HOLLight.hollight.HAS_SIZE_FINITE_IMAGE"
  1391   "HAS_SIZE_CLAUSES" > "HOLLight.hollight.HAS_SIZE_CLAUSES"
  1392   "HAS_SIZE_CARD" > "HOLLight.hollight.HAS_SIZE_CARD"
  1393   "HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
  1394   "GSPEC_def" > "HOLLight.hollight.GSPEC_def"
  1395   "GEQ_def" > "HOLLight.hollight.GEQ_def"
  1396   "GABS_def" > "HOLLight.hollight.GABS_def"
  1397   "FUN_EQ_THM" > "Fun.fun_eq_iff"
  1398   "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
  1399   "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
  1400   "FSTCART_PASTECART" > "HOLLight.hollight.FSTCART_PASTECART"
  1401   "FST" > "Product_Type.fst_conv"
  1402   "FORALL_SIMP" > "HOL.simp_thms_35"
  1403   "FORALL_PASTECART" > "HOLLight.hollight.FORALL_PASTECART"
  1404   "FORALL_PAIR_THM" > "Product_Type.split_paired_All"
  1405   "FORALL_NOT_THM" > "Inductive.basic_monos_16"
  1406   "FORALL_IN_UNIONS" > "HOLLight.hollight.FORALL_IN_UNIONS"
  1407   "FORALL_IN_IMAGE" > "HOLLight.hollight.FORALL_IN_IMAGE"
  1408   "FORALL_IN_CLAUSES" > "HOLLight.hollight.FORALL_IN_CLAUSES"
  1409   "FORALL_FINITE_INDEX" > "HOLLight.hollight.FORALL_FINITE_INDEX"
  1410   "FORALL_BOOL_THM" > "Set.all_bool_eq"
  1411   "FORALL_AND_THM" > "HOL.all_conj_distrib"
  1412   "FORALL_ALL" > "HOLLight.hollight.FORALL_ALL"
  1413   "FNIL_def" > "HOLLight.hollight.FNIL_def"
  1414   "FINREC_def" > "HOLLight.hollight.FINREC_def"
  1415   "FINREC_UNIQUE_LEMMA" > "HOLLight.hollight.FINREC_UNIQUE_LEMMA"
  1416   "FINREC_SUC_LEMMA" > "HOLLight.hollight.FINREC_SUC_LEMMA"
  1417   "FINREC_FUN_LEMMA" > "HOLLight.hollight.FINREC_FUN_LEMMA"
  1418   "FINREC_FUN" > "HOLLight.hollight.FINREC_FUN"
  1419   "FINREC_EXISTS_LEMMA" > "HOLLight.hollight.FINREC_EXISTS_LEMMA"
  1420   "FINREC_1_LEMMA" > "HOLLight.hollight.FINREC_1_LEMMA"
  1421   "FINITE_def" > "HOLLight.hollight.FINITE_def"
  1422   "FINITE_UNION_IMP" > "HOLLight.hollight.FINITE_UNION_IMP"
  1423   "FINITE_UNIONS" > "HOLLight.hollight.FINITE_UNIONS"
  1424   "FINITE_UNION" > "HOLLight.hollight.FINITE_UNION"
  1425   "FINITE_SUPPORT_DELTA" > "HOLLight.hollight.FINITE_SUPPORT_DELTA"
  1426   "FINITE_SUPPORT" > "HOLLight.hollight.FINITE_SUPPORT"
  1427   "FINITE_SUBSET_IMAGE_IMP" > "HOLLight.hollight.FINITE_SUBSET_IMAGE_IMP"
  1428   "FINITE_SUBSET_IMAGE" > "HOLLight.hollight.FINITE_SUBSET_IMAGE"
  1429   "FINITE_SUBSETS" > "HOLLight.hollight.FINITE_SUBSETS"
  1430   "FINITE_SUBSET" > "HOLLight.hollight.FINITE_SUBSET"
  1431   "FINITE_SET_OF_LIST" > "HOLLight.hollight.FINITE_SET_OF_LIST"
  1432   "FINITE_RESTRICT" > "HOLLight.hollight.FINITE_RESTRICT"
  1433   "FINITE_RECURSION_DELETE" > "HOLLight.hollight.FINITE_RECURSION_DELETE"
  1434   "FINITE_RECURSION" > "HOLLight.hollight.FINITE_RECURSION"
  1435   "FINITE_PRODUCT_DEPENDENT" > "HOLLight.hollight.FINITE_PRODUCT_DEPENDENT"
  1436   "FINITE_PRODUCT" > "HOLLight.hollight.FINITE_PRODUCT"
  1437   "FINITE_POWERSET" > "HOLLight.hollight.FINITE_POWERSET"
  1438   "FINITE_NUMSEG_LT" > "HOLLight.hollight.FINITE_NUMSEG_LT"
  1439   "FINITE_NUMSEG_LE" > "HOLLight.hollight.FINITE_NUMSEG_LE"
  1440   "FINITE_NUMSEG" > "HOLLight.hollight.FINITE_NUMSEG"
  1441   "FINITE_INTER" > "HOLLight.hollight.FINITE_INTER"
  1442   "FINITE_INSERT" > "HOLLight.hollight.FINITE_INSERT"
  1443   "FINITE_INDUCT_STRONG" > "HOLLight.hollight.FINITE_INDUCT_STRONG"
  1444   "FINITE_INDEX_WORKS_FINITE" > "HOLLight.hollight.FINITE_INDEX_WORKS_FINITE"
  1445   "FINITE_INDEX_WORKS" > "HOLLight.hollight.FINITE_INDEX_WORKS"
  1446   "FINITE_INDEX_NUMSEG" > "HOLLight.hollight.FINITE_INDEX_NUMSEG"
  1447   "FINITE_INDEX_NUMBERS" > "HOLLight.hollight.FINITE_INDEX_NUMBERS"
  1448   "FINITE_INDEX_INJ" > "HOLLight.hollight.FINITE_INDEX_INJ"
  1449   "FINITE_IMAGE_INJ_GENERAL" > "HOLLight.hollight.FINITE_IMAGE_INJ_GENERAL"
  1450   "FINITE_IMAGE_INJ" > "HOLLight.hollight.FINITE_IMAGE_INJ"
  1451   "FINITE_IMAGE_IMAGE" > "HOLLight.hollight.FINITE_IMAGE_IMAGE"
  1452   "FINITE_IMAGE_EXPAND" > "HOLLight.hollight.FINITE_IMAGE_EXPAND"
  1453   "FINITE_IMAGE" > "HOLLight.hollight.FINITE_IMAGE"
  1454   "FINITE_HAS_SIZE_LEMMA" > "HOLLight.hollight.FINITE_HAS_SIZE_LEMMA"
  1455   "FINITE_FUNSPACE" > "HOLLight.hollight.FINITE_FUNSPACE"
  1456   "FINITE_FINITE_IMAGE" > "HOLLight.hollight.FINITE_FINITE_IMAGE"
  1457   "FINITE_DIFF" > "HOLLight.hollight.FINITE_DIFF"
  1458   "FINITE_DELETE_IMP" > "HOLLight.hollight.FINITE_DELETE_IMP"
  1459   "FINITE_DELETE" > "HOLLight.hollight.FINITE_DELETE"
  1460   "FILTER_def" > "HOLLight.hollight.FILTER_def"
  1461   "FILTER_MAP" > "HOLLight.hollight.FILTER_MAP"
  1462   "FILTER_APPEND" > "HOLLight.hollight.FILTER_APPEND"
  1463   "FCONS_def" > "HOLLight.hollight.FCONS_def"
  1464   "FCONS_UNDO" > "HOLLight.hollight.FCONS_UNDO"
  1465   "FACT_def" > "HOLLight.hollight.FACT_def"
  1466   "FACT_MONO" > "HOLLight.hollight.FACT_MONO"
  1467   "FACT_LT" > "HOLLight.hollight.FACT_LT"
  1468   "FACT_LE" > "HOLLight.hollight.FACT_LE"
  1469   "EX_def" > "HOLLight.hollight.EX_def"
  1470   "EX_MEM" > "HOLLight.hollight.EX_MEM"
  1471   "EX_MAP" > "HOLLight.hollight.EX_MAP"
  1472   "EX_IMP" > "HOLLight.hollight.EX_IMP"
  1473   "EXTENSION" > "HOLLight.hollight.EXTENSION"
  1474   "EXP_def" > "HOLLight.hollight.EXP_def"
  1475   "EXP_ONE" > "HOLLight.hollight.EXP_ONE"
  1476   "EXP_MULT" > "HOLLight.hollight.EXP_MULT"
  1477   "EXP_LT_0" > "HOLLight.hollight.EXP_LT_0"
  1478   "EXP_EQ_0" > "HOLLight.hollight.EXP_EQ_0"
  1479   "EXP_ADD" > "HOLLight.hollight.EXP_ADD"
  1480   "EXP_2" > "HOLLight.hollight.EXP_2"
  1481   "EXP_1" > "HOLLight.hollight.EXP_1"
  1482   "EXISTS_UNIQUE_THM" > "HOL4Compat.EXISTS_UNIQUE_DEF"
  1483   "EXISTS_UNIQUE_REFL" > "HOL.ex1_eq_1"
  1484   "EXISTS_UNIQUE_ALT" > "HOLLight.hollight.EXISTS_UNIQUE_ALT"
  1485   "EXISTS_UNIQUE" > "HOL.Ex1_def"
  1486   "EXISTS_THM" > "HOL4Setup.EXISTS_DEF"
  1487   "EXISTS_SIMP" > "HOL.simp_thms_36"
  1488   "EXISTS_REFL" > "HOL.simp_thms_37"
  1489   "EXISTS_PASTECART" > "HOLLight.hollight.EXISTS_PASTECART"
  1490   "EXISTS_PAIR_THM" > "Product_Type.split_paired_Ex"
  1491   "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
  1492   "EXISTS_ONE_REP" > "HOLLight.hollight.EXISTS_ONE_REP"
  1493   "EXISTS_NOT_THM" > "Inductive.basic_monos_15"
  1494   "EXISTS_IN_IMAGE" > "HOLLight.hollight.EXISTS_IN_IMAGE"
  1495   "EXISTS_IN_CLAUSES" > "HOLLight.hollight.EXISTS_IN_CLAUSES"
  1496   "EXISTS_EX" > "HOLLight.hollight.EXISTS_EX"
  1497   "EXISTS_BOOL_THM" > "Set.ex_bool_eq"
  1498   "EXCLUDED_MIDDLE" > "HOLLight.hollight.EXCLUDED_MIDDLE"
  1499   "EVEN_def" > "HOLLight.hollight.EVEN_def"
  1500   "EVEN_OR_ODD" > "HOLLight.hollight.EVEN_OR_ODD"
  1501   "EVEN_ODD_DECOMPOSITION" > "HOLLight.hollight.EVEN_ODD_DECOMPOSITION"
  1502   "EVEN_MULT" > "HOLLight.hollight.EVEN_MULT"
  1503   "EVEN_MOD" > "HOLLight.hollight.EVEN_MOD"
  1504   "EVEN_EXP" > "HOLLight.hollight.EVEN_EXP"
  1505   "EVEN_EXISTS_LEMMA" > "HOLLight.hollight.EVEN_EXISTS_LEMMA"
  1506   "EVEN_EXISTS" > "HOLLight.hollight.EVEN_EXISTS"
  1507   "EVEN_DOUBLE" > "HOLLight.hollight.EVEN_DOUBLE"
  1508   "EVEN_AND_ODD" > "HOLLight.hollight.EVEN_AND_ODD"
  1509   "EVEN_ADD" > "HOLLight.hollight.EVEN_ADD"
  1510   "EQ_UNIV" > "HOLLight.hollight.EQ_UNIV"
  1511   "EQ_TRANS" > "Set.basic_trans_rules_31"
  1512   "EQ_SYM_EQ" > "HOL.eq_sym_conv"
  1513   "EQ_SYM" > "HOL.meta_eq_to_obj_eq"
  1514   "EQ_SUC" > "Nat.nat.simps_3"
  1515   "EQ_REFL_T" > "HOL.simp_thms_6"
  1516   "EQ_REFL" > "Presburger.fm_modd_pinf"
  1517   "EQ_MULT_RCANCEL" > "Nat.mult_cancel2"
  1518   "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
  1519   "EQ_IMP_LE" > "HOLLight.hollight.EQ_IMP_LE"
  1520   "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
  1521   "EQ_CLAUSES" > "HOLLight.hollight.EQ_CLAUSES"
  1522   "EQ_ADD_RCANCEL_0" > "HOLLight.hollight.EQ_ADD_RCANCEL_0"
  1523   "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
  1524   "EQ_ADD_LCANCEL_0" > "HOLLight.hollight.EQ_ADD_LCANCEL_0"
  1525   "EQ_ADD_LCANCEL" > "Nat.nat_add_left_cancel"
  1526   "EMPTY_def" > "HOLLight.hollight.EMPTY_def"
  1527   "EMPTY_UNIONS" > "HOLLight.hollight.EMPTY_UNIONS"
  1528   "EMPTY_UNION" > "HOLLight.hollight.EMPTY_UNION"
  1529   "EMPTY_SUBSET" > "HOLLight.hollight.EMPTY_SUBSET"
  1530   "EMPTY_NOT_UNIV" > "HOLLight.hollight.EMPTY_NOT_UNIV"
  1531   "EMPTY_GSPEC" > "HOLLight.hollight.EMPTY_GSPEC"
  1532   "EMPTY_DIFF" > "HOLLight.hollight.EMPTY_DIFF"
  1533   "EMPTY_DELETE" > "HOLLight.hollight.EMPTY_DELETE"
  1534   "EL_def" > "HOLLight.hollight.EL_def"
  1535   "DIV_def" > "HOLLight.hollight.DIV_def"
  1536   "DIV_UNIQ" > "HOLLight.hollight.DIV_UNIQ"
  1537   "DIV_REFL" > "HOLLight.hollight.DIV_REFL"
  1538   "DIV_MUL_LE" > "HOLLight.hollight.DIV_MUL_LE"
  1539   "DIV_MULT2" > "HOLLight.hollight.DIV_MULT2"
  1540   "DIV_MULT" > "HOLLight.hollight.DIV_MULT"
  1541   "DIV_MONO_LT" > "HOLLight.hollight.DIV_MONO_LT"
  1542   "DIV_MONO2" > "HOLLight.hollight.DIV_MONO2"
  1543   "DIV_MONO" > "HOLLight.hollight.DIV_MONO"
  1544   "DIV_MOD" > "HOLLight.hollight.DIV_MOD"
  1545   "DIV_LT" > "HOLLight.hollight.DIV_LT"
  1546   "DIV_LE_EXCLUSION" > "HOLLight.hollight.DIV_LE_EXCLUSION"
  1547   "DIV_LE" > "HOLLight.hollight.DIV_LE"
  1548   "DIV_EQ_EXCLUSION" > "HOLLight.hollight.DIV_EQ_EXCLUSION"
  1549   "DIV_EQ_0" > "HOLLight.hollight.DIV_EQ_0"
  1550   "DIV_DIV" > "HOLLight.hollight.DIV_DIV"
  1551   "DIV_ADD_MOD" > "HOLLight.hollight.DIV_ADD_MOD"
  1552   "DIV_1" > "HOLLight.hollight.DIV_1"
  1553   "DIV_0" > "HOLLight.hollight.DIV_0"
  1554   "DIVMOD_UNIQ_LEMMA" > "HOLLight.hollight.DIVMOD_UNIQ_LEMMA"
  1555   "DIVMOD_UNIQ" > "HOLLight.hollight.DIVMOD_UNIQ"
  1556   "DIVMOD_EXIST_0" > "HOLLight.hollight.DIVMOD_EXIST_0"
  1557   "DIVMOD_EXIST" > "HOLLight.hollight.DIVMOD_EXIST"
  1558   "DIVMOD_ELIM_THM" > "HOLLight.hollight.DIVMOD_ELIM_THM"
  1559   "DIVISION" > "HOLLight.hollight.DIVISION"
  1560   "DIST_TRIANGLE_LE" > "HOLLight.hollight.DIST_TRIANGLE_LE"
  1561   "DIST_TRIANGLES_LE" > "HOLLight.hollight.DIST_TRIANGLES_LE"
  1562   "DIST_TRIANGLE" > "HOLLight.hollight.DIST_TRIANGLE"
  1563   "DIST_SYM" > "HOLLight.hollight.DIST_SYM"
  1564   "DIST_RZERO" > "HOLLight.hollight.DIST_RZERO"
  1565   "DIST_RMUL" > "HOLLight.hollight.DIST_RMUL"
  1566   "DIST_REFL" > "HOLLight.hollight.DIST_REFL"
  1567   "DIST_RADD_0" > "HOLLight.hollight.DIST_RADD_0"
  1568   "DIST_RADD" > "HOLLight.hollight.DIST_RADD"
  1569   "DIST_LZERO" > "HOLLight.hollight.DIST_LZERO"
  1570   "DIST_LMUL" > "HOLLight.hollight.DIST_LMUL"
  1571   "DIST_LE_CASES" > "HOLLight.hollight.DIST_LE_CASES"
  1572   "DIST_LADD_0" > "HOLLight.hollight.DIST_LADD_0"
  1573   "DIST_LADD" > "HOLLight.hollight.DIST_LADD"
  1574   "DIST_EQ_0" > "HOLLight.hollight.DIST_EQ_0"
  1575   "DIST_ELIM_THM" > "HOLLight.hollight.DIST_ELIM_THM"
  1576   "DIST_ADDBOUND" > "HOLLight.hollight.DIST_ADDBOUND"
  1577   "DIST_ADD2_REV" > "HOLLight.hollight.DIST_ADD2_REV"
  1578   "DIST_ADD2" > "HOLLight.hollight.DIST_ADD2"
  1579   "DISJ_SYM" > "HOL.disj_comms_1"
  1580   "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
  1581   "DISJ_ACI" > "HOLLight.hollight.DISJ_ACI"
  1582   "DISJOINT_def" > "HOLLight.hollight.DISJOINT_def"
  1583   "DISJOINT_UNION" > "HOLLight.hollight.DISJOINT_UNION"
  1584   "DISJOINT_SYM" > "HOLLight.hollight.DISJOINT_SYM"
  1585   "DISJOINT_NUMSEG" > "HOLLight.hollight.DISJOINT_NUMSEG"
  1586   "DISJOINT_INSERT" > "HOLLight.hollight.DISJOINT_INSERT"
  1587   "DISJOINT_EMPTY_REFL" > "HOLLight.hollight.DISJOINT_EMPTY_REFL"
  1588   "DISJOINT_EMPTY" > "HOLLight.hollight.DISJOINT_EMPTY"
  1589   "DISJOINT_DELETE_SYM" > "HOLLight.hollight.DISJOINT_DELETE_SYM"
  1590   "DIMINDEX_NONZERO" > "HOLLight.hollight.DIMINDEX_NONZERO"
  1591   "DIMINDEX_HAS_SIZE_FINITE_SUM" > "HOLLight.hollight.DIMINDEX_HAS_SIZE_FINITE_SUM"
  1592   "DIMINDEX_GE_1" > "HOLLight.hollight.DIMINDEX_GE_1"
  1593   "DIMINDEX_FINITE_SUM" > "HOLLight.hollight.DIMINDEX_FINITE_SUM"
  1594   "DIMINDEX_FINITE_IMAGE" > "HOLLight.hollight.DIMINDEX_FINITE_IMAGE"
  1595   "DIFF_def" > "HOLLight.hollight.DIFF_def"
  1596   "DIFF_UNIV" > "HOLLight.hollight.DIFF_UNIV"
  1597   "DIFF_INSERT" > "HOLLight.hollight.DIFF_INSERT"
  1598   "DIFF_EQ_EMPTY" > "HOLLight.hollight.DIFF_EQ_EMPTY"
  1599   "DIFF_EMPTY" > "HOLLight.hollight.DIFF_EMPTY"
  1600   "DIFF_DIFF" > "HOLLight.hollight.DIFF_DIFF"
  1601   "DEST_REC_INJ" > "HOLLight.hollight.recspace._dest_rec_inject"
  1602   "DELETE_def" > "HOLLight.hollight.DELETE_def"
  1603   "DELETE_SUBSET" > "HOLLight.hollight.DELETE_SUBSET"
  1604   "DELETE_NON_ELEMENT" > "HOLLight.hollight.DELETE_NON_ELEMENT"
  1605   "DELETE_INTER" > "HOLLight.hollight.DELETE_INTER"
  1606   "DELETE_INSERT" > "HOLLight.hollight.DELETE_INSERT"
  1607   "DELETE_DELETE" > "HOLLight.hollight.DELETE_DELETE"
  1608   "DELETE_COMM" > "HOLLight.hollight.DELETE_COMM"
  1609   "DEF_~" > "HOL.simp_thms_19"
  1610   "DEF_two_2" > "HOLLight.hollight.DEF_two_2"
  1611   "DEF_two_1" > "HOLLight.hollight.DEF_two_1"
  1612   "DEF_treal_of_num" > "HOLLight.hollight.DEF_treal_of_num"
  1613   "DEF_treal_neg" > "HOLLight.hollight.DEF_treal_neg"
  1614   "DEF_treal_mul" > "HOLLight.hollight.DEF_treal_mul"
  1615   "DEF_treal_le" > "HOLLight.hollight.DEF_treal_le"
  1616   "DEF_treal_inv" > "HOLLight.hollight.DEF_treal_inv"
  1617   "DEF_treal_eq" > "HOLLight.hollight.DEF_treal_eq"
  1618   "DEF_treal_add" > "HOLLight.hollight.DEF_treal_add"
  1619   "DEF_three_3" > "HOLLight.hollight.DEF_three_3"
  1620   "DEF_three_2" > "HOLLight.hollight.DEF_three_2"
  1621   "DEF_three_1" > "HOLLight.hollight.DEF_three_1"
  1622   "DEF_tailadmissible" > "HOLLight.hollight.DEF_tailadmissible"
  1623   "DEF_support" > "HOLLight.hollight.DEF_support"
  1624   "DEF_superadmissible" > "HOLLight.hollight.DEF_superadmissible"
  1625   "DEF_sum" > "HOLLight.hollight.DEF_sum"
  1626   "DEF_sndcart" > "HOLLight.hollight.DEF_sndcart"
  1627   "DEF_set_of_list" > "HOLLight.hollight.DEF_set_of_list"
  1628   "DEF_real_sub" > "HOLLight.hollight.DEF_real_sub"
  1629   "DEF_real_pow" > "HOLLight.hollight.DEF_real_pow"
  1630   "DEF_real_of_num" > "HOLLight.hollight.DEF_real_of_num"
  1631   "DEF_real_neg" > "HOLLight.hollight.DEF_real_neg"
  1632   "DEF_real_mul" > "HOLLight.hollight.DEF_real_mul"
  1633   "DEF_real_min" > "HOLLight.hollight.DEF_real_min"
  1634   "DEF_real_max" > "HOLLight.hollight.DEF_real_max"
  1635   "DEF_real_lt" > "HOLLight.hollight.DEF_real_lt"
  1636   "DEF_real_le" > "HOLLight.hollight.DEF_real_le"
  1637   "DEF_real_inv" > "HOLLight.hollight.DEF_real_inv"
  1638   "DEF_real_gt" > "HOLLight.hollight.DEF_real_gt"
  1639   "DEF_real_ge" > "HOLLight.hollight.DEF_real_ge"
  1640   "DEF_real_div" > "HOLLight.hollight.DEF_real_div"
  1641   "DEF_real_add" > "HOLLight.hollight.DEF_real_add"
  1642   "DEF_real_abs" > "HOLLight.hollight.DEF_real_abs"
  1643   "DEF_pastecart" > "HOLLight.hollight.DEF_pastecart"
  1644   "DEF_pairwise" > "HOLLight.hollight.DEF_pairwise"
  1645   "DEF_o" > "Fun.o_apply"
  1646   "DEF_nsum" > "HOLLight.hollight.DEF_nsum"
  1647   "DEF_neutral" > "HOLLight.hollight.DEF_neutral"
  1648   "DEF_nadd_rinv" > "HOLLight.hollight.DEF_nadd_rinv"
  1649   "DEF_nadd_of_num" > "HOLLight.hollight.DEF_nadd_of_num"
  1650   "DEF_nadd_mul" > "HOLLight.hollight.DEF_nadd_mul"
  1651   "DEF_nadd_le" > "HOLLight.hollight.DEF_nadd_le"
  1652   "DEF_nadd_inv" > "HOLLight.hollight.DEF_nadd_inv"
  1653   "DEF_nadd_eq" > "HOLLight.hollight.DEF_nadd_eq"
  1654   "DEF_nadd_add" > "HOLLight.hollight.DEF_nadd_add"
  1655   "DEF_monoidal" > "HOLLight.hollight.DEF_monoidal"
  1656   "DEF_mod_real" > "HOLLight.hollight.DEF_mod_real"
  1657   "DEF_mod_nat" > "HOLLight.hollight.DEF_mod_nat"
  1658   "DEF_mod_int" > "HOLLight.hollight.DEF_mod_int"
  1659   "DEF_mk_pair" > "Product_Type.Pair_Rep_def"
  1660   "DEF_minimal" > "HOLLight.hollight.DEF_minimal"
  1661   "DEF_measure" > "HOLLight.hollight.DEF_measure"
  1662   "DEF_list_of_set" > "HOLLight.hollight.DEF_list_of_set"
  1663   "DEF_lambda" > "HOLLight.hollight.DEF_lambda"
  1664   "DEF_iterate" > "HOLLight.hollight.DEF_iterate"
  1665   "DEF_is_nadd" > "HOLLight.hollight.DEF_is_nadd"
  1666   "DEF_is_int" > "HOLLight.hollight.DEF_is_int"
  1667   "DEF_int_sub" > "HOLLight.hollight.DEF_int_sub"
  1668   "DEF_int_pow" > "HOLLight.hollight.DEF_int_pow"
  1669   "DEF_int_of_num" > "HOLLight.hollight.DEF_int_of_num"
  1670   "DEF_int_neg" > "HOLLight.hollight.DEF_int_neg"
  1671   "DEF_int_mul" > "HOLLight.hollight.DEF_int_mul"
  1672   "DEF_int_min" > "HOLLight.hollight.DEF_int_min"
  1673   "DEF_int_max" > "HOLLight.hollight.DEF_int_max"
  1674   "DEF_int_lt" > "HOLLight.hollight.DEF_int_lt"
  1675   "DEF_int_le" > "HOLLight.hollight.DEF_int_le"
  1676   "DEF_int_gt" > "HOLLight.hollight.DEF_int_gt"
  1677   "DEF_int_ge" > "HOLLight.hollight.DEF_int_ge"
  1678   "DEF_int_add" > "HOLLight.hollight.DEF_int_add"
  1679   "DEF_int_abs" > "HOLLight.hollight.DEF_int_abs"
  1680   "DEF_hreal_of_num" > "HOLLight.hollight.DEF_hreal_of_num"
  1681   "DEF_hreal_mul" > "HOLLight.hollight.DEF_hreal_mul"
  1682   "DEF_hreal_le" > "HOLLight.hollight.DEF_hreal_le"
  1683   "DEF_hreal_inv" > "HOLLight.hollight.DEF_hreal_inv"
  1684   "DEF_hreal_add" > "HOLLight.hollight.DEF_hreal_add"
  1685   "DEF_fstcart" > "HOLLight.hollight.DEF_fstcart"
  1686   "DEF_finite_index" > "HOLLight.hollight.DEF_finite_index"
  1687   "DEF_dist" > "HOLLight.hollight.DEF_dist"
  1688   "DEF_dimindex" > "HOLLight.hollight.DEF_dimindex"
  1689   "DEF_admissible" > "HOLLight.hollight.DEF_admissible"
  1690   "DEF__star_" > "HOLLightCompat.mult_altdef"
  1691   "DEF__slash__backslash_" > "HOLLightCompat.light_and_def"
  1692   "DEF__questionmark__exclamationmark_" > "HOL4Compat.EXISTS_UNIQUE_DEF"
  1693   "DEF__questionmark_" > "HOL.Ex_def"
  1694   "DEF__lessthan__equal_" > "HOLLight.hollight.DEF__lessthan__equal_"
  1695   "DEF__lessthan_" > "HOLLight.hollight.DEF__lessthan_"
  1696   "DEF__greaterthan__equal_" > "HOLLight.hollight.DEF__greaterthan__equal_"
  1697   "DEF__greaterthan_" > "HOLLight.hollight.DEF__greaterthan_"
  1698   "DEF__exclamationmark_" > "HOL.All_def"
  1699   "DEF__equal__equal__greaterthan_" > "HOLLightCompat.light_imp_def"
  1700   "DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
  1701   "DEF__dot__dot_" > "HOLLight.hollight.DEF__dot__dot_"
  1702   "DEF__backslash__slash_" > "HOL.or_def"
  1703   "DEF__FALSITY_" > "HOLLight.hollight.DEF__FALSITY_"
  1704   "DEF__10328" > "HOLLight.hollight.DEF__10328"
  1705   "DEF__10327" > "HOLLight.hollight.DEF__10327"
  1706   "DEF__10326" > "HOLLight.hollight.DEF__10326"
  1707   "DEF__10303" > "HOLLight.hollight.DEF__10303"
  1708   "DEF__10302" > "HOLLight.hollight.DEF__10302"
  1709   "DEF_ZRECSPACE" > "HOLLight.hollight.DEF_ZRECSPACE"
  1710   "DEF_ZIP" > "HOLLight.hollight.DEF_ZIP"
  1711   "DEF_ZCONSTR" > "HOLLight.hollight.DEF_ZCONSTR"
  1712   "DEF_ZBOT" > "HOLLight.hollight.DEF_ZBOT"
  1713   "DEF_WF" > "HOLLight.hollight.DEF_WF"
  1714   "DEF_UNIV" > "HOLLight.hollight.DEF_UNIV"
  1715   "DEF_UNIONS" > "HOLLight.hollight.DEF_UNIONS"
  1716   "DEF_UNION" > "HOLLight.hollight.DEF_UNION"
  1717   "DEF_UNCURRY" > "HOLLight.hollight.DEF_UNCURRY"
  1718   "DEF_TL" > "HOLLight.hollight.DEF_TL"
  1719   "DEF_T" > "HOL.True_def"
  1720   "DEF_SURJ" > "HOLLight.hollight.DEF_SURJ"
  1721   "DEF_SUBSET" > "HOLLight.hollight.DEF_SUBSET"
  1722   "DEF_SOME" > "HOLLight.hollight.DEF_SOME"
  1723   "DEF_SND" > "HOLLightCompat.snd_altdef"
  1724   "DEF_SING" > "HOLLight.hollight.DEF_SING"
  1725   "DEF_SETSPEC" > "HOLLight.hollight.DEF_SETSPEC"
  1726   "DEF_REVERSE" > "HOLLight.hollight.DEF_REVERSE"
  1727   "DEF_REST" > "HOLLight.hollight.DEF_REST"
  1728   "DEF_REPLICATE" > "HOLLight.hollight.DEF_REPLICATE"
  1729   "DEF_PSUBSET" > "HOLLight.hollight.DEF_PSUBSET"
  1730   "DEF_PRE" > "HOLLightCompat.Pred_altdef"
  1731   "DEF_PASSOC" > "HOLLight.hollight.DEF_PASSOC"
  1732   "DEF_PAIRWISE" > "HOLLight.hollight.DEF_PAIRWISE"
  1733   "DEF_OUTR" > "HOLLight.hollight.DEF_OUTR"
  1734   "DEF_OUTL" > "HOLLight.hollight.DEF_OUTL"
  1735   "DEF_ONTO" > "Fun.surj_def"
  1736   "DEF_ONE_ONE" > "HOL4Setup.ONE_ONE_DEF"
  1737   "DEF_ODD" > "HOLLight.hollight.DEF_ODD"
  1738   "DEF_NUMSUM" > "HOLLight.hollight.DEF_NUMSUM"
  1739   "DEF_NUMSND" > "HOLLight.hollight.DEF_NUMSND"
  1740   "DEF_NUMRIGHT" > "HOLLight.hollight.DEF_NUMRIGHT"
  1741   "DEF_NUMPAIR" > "HOLLight.hollight.DEF_NUMPAIR"
  1742   "DEF_NUMLEFT" > "HOLLight.hollight.DEF_NUMLEFT"
  1743   "DEF_NUMFST" > "HOLLight.hollight.DEF_NUMFST"
  1744   "DEF_NUMERAL" > "HOLLightCompat.NUMERAL_rew"
  1745   "DEF_NULL" > "HOLLight.hollight.DEF_NULL"
  1746   "DEF_NONE" > "HOLLight.hollight.DEF_NONE"
  1747   "DEF_NIL" > "HOLLight.hollight.DEF_NIL"
  1748   "DEF_MOD" > "HOLLight.hollight.DEF_MOD"
  1749   "DEF_MEM" > "HOLLight.hollight.DEF_MEM"
  1750   "DEF_MAP2" > "HOLLight.hollight.DEF_MAP2"
  1751   "DEF_MAP" > "HOLLight.hollight.DEF_MAP"
  1752   "DEF_LET_END" > "HOLLight.hollight.DEF_LET_END"
  1753   "DEF_LET" > "HOL4Compat.LET_def"
  1754   "DEF_LENGTH" > "HOLLight.hollight.DEF_LENGTH"
  1755   "DEF_LAST" > "HOLLight.hollight.DEF_LAST"
  1756   "DEF_ITSET" > "HOLLight.hollight.DEF_ITSET"
  1757   "DEF_ITLIST2" > "HOLLight.hollight.DEF_ITLIST2"
  1758   "DEF_ITLIST" > "HOLLight.hollight.DEF_ITLIST"
  1759   "DEF_ISO" > "HOLLight.hollight.DEF_ISO"
  1760   "DEF_INTERS" > "HOLLight.hollight.DEF_INTERS"
  1761   "DEF_INTER" > "HOLLight.hollight.DEF_INTER"
  1762   "DEF_INSERT" > "HOLLight.hollight.DEF_INSERT"
  1763   "DEF_INJP" > "HOLLight.hollight.DEF_INJP"
  1764   "DEF_INJN" > "HOLLight.hollight.DEF_INJN"
  1765   "DEF_INJF" > "HOLLight.hollight.DEF_INJF"
  1766   "DEF_INJA" > "HOLLight.hollight.DEF_INJA"
  1767   "DEF_INJ" > "HOLLight.hollight.DEF_INJ"
  1768   "DEF_INFINITE" > "HOLLight.hollight.DEF_INFINITE"
  1769   "DEF_IN" > "HOLLight.hollight.DEF_IN"
  1770   "DEF_IMAGE" > "HOLLight.hollight.DEF_IMAGE"
  1771   "DEF_I" > "Fun.id_apply"
  1772   "DEF_HD" > "HOLLight.hollight.DEF_HD"
  1773   "DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
  1774   "DEF_GSPEC" > "HOLLight.hollight.DEF_GSPEC"
  1775   "DEF_GEQ" > "HOLLight.hollight.DEF_GEQ"
  1776   "DEF_GABS" > "HOLLight.hollight.DEF_GABS"
  1777   "DEF_FST" > "HOLLightCompat.fst_altdef"
  1778   "DEF_FNIL" > "HOLLight.hollight.DEF_FNIL"
  1779   "DEF_FINREC" > "HOLLight.hollight.DEF_FINREC"
  1780   "DEF_FINITE" > "HOLLight.hollight.DEF_FINITE"
  1781   "DEF_FILTER" > "HOLLight.hollight.DEF_FILTER"
  1782   "DEF_FCONS" > "HOLLight.hollight.DEF_FCONS"
  1783   "DEF_FACT" > "HOLLight.hollight.DEF_FACT"
  1784   "DEF_F" > "HOL.False_def"
  1785   "DEF_EXP" > "HOLLight.hollight.DEF_EXP"
  1786   "DEF_EX" > "HOLLight.hollight.DEF_EX"
  1787   "DEF_EVEN" > "HOLLight.hollight.DEF_EVEN"
  1788   "DEF_EMPTY" > "HOLLight.hollight.DEF_EMPTY"
  1789   "DEF_EL" > "HOLLight.hollight.DEF_EL"
  1790   "DEF_DIV" > "HOLLight.hollight.DEF_DIV"
  1791   "DEF_DISJOINT" > "HOLLight.hollight.DEF_DISJOINT"
  1792   "DEF_DIFF" > "HOLLight.hollight.DEF_DIFF"
  1793   "DEF_DELETE" > "HOLLight.hollight.DEF_DELETE"
  1794   "DEF_DECIMAL" > "HOLLight.hollight.DEF_DECIMAL"
  1795   "DEF_CURRY" > "HOLLight.hollight.DEF_CURRY"
  1796   "DEF_COUNTABLE" > "HOLLight.hollight.DEF_COUNTABLE"
  1797   "DEF_CONSTR" > "HOLLight.hollight.DEF_CONSTR"
  1798   "DEF_CONS" > "HOLLight.hollight.DEF_CONS"
  1799   "DEF_COND" > "HOLLight.hollight.DEF_COND"
  1800   "DEF_CHOICE" > "HOLLight.hollight.DEF_CHOICE"
  1801   "DEF_CASEWISE" > "HOLLight.hollight.DEF_CASEWISE"
  1802   "DEF_CARD_LT" > "HOLLight.hollight.DEF_CARD_LT"
  1803   "DEF_CARD_LE" > "HOLLight.hollight.DEF_CARD_LE"
  1804   "DEF_CARD_GT" > "HOLLight.hollight.DEF_CARD_GT"
  1805   "DEF_CARD_GE" > "HOLLight.hollight.DEF_CARD_GE"
  1806   "DEF_CARD_EQ" > "HOLLight.hollight.DEF_CARD_EQ"
  1807   "DEF_CARD" > "HOLLight.hollight.DEF_CARD"
  1808   "DEF_BOTTOM" > "HOLLight.hollight.DEF_BOTTOM"
  1809   "DEF_BIT1" > "HOLLightCompat.NUMERAL_BIT1_altdef"
  1810   "DEF_BIT0" > "HOLLightCompat.NUMERAL_BIT0_def"
  1811   "DEF_BIJ" > "HOLLight.hollight.DEF_BIJ"
  1812   "DEF_ASSOC" > "HOLLight.hollight.DEF_ASSOC"
  1813   "DEF_APPEND" > "HOLLight.hollight.DEF_APPEND"
  1814   "DEF_ALL2" > "HOLLight.hollight.DEF_ALL2"
  1815   "DEF_ALL" > "HOLLight.hollight.DEF_ALL"
  1816   "DEF_-" > "HOLLightCompat.sub_altdef"
  1817   "DEF_," > "Product_Type.Pair_def"
  1818   "DEF_+" > "HOLLightCompat.add_altdef"
  1819   "DEF_$" > "HOLLight.hollight.DEF_$"
  1820   "DECOMPOSITION" > "HOLLight.hollight.DECOMPOSITION"
  1821   "DECIMAL_def" > "HOLLight.hollight.DECIMAL_def"
  1822   "CURRY_def" > "HOLLight.hollight.CURRY_def"
  1823   "COUNTABLE_def" > "HOLLight.hollight.COUNTABLE_def"
  1824   "CONS_def" > "HOLLight.hollight.CONS_def"
  1825   "CONS_11" > "HOLLight.hollight.CONS_11"
  1826   "CONSTR_def" > "HOLLight.hollight.CONSTR_def"
  1827   "CONSTR_REC" > "HOLLight.hollight.CONSTR_REC"
  1828   "CONSTR_INJ" > "HOLLight.hollight.CONSTR_INJ"
  1829   "CONSTR_IND" > "HOLLight.hollight.CONSTR_IND"
  1830   "CONSTR_BOT" > "HOLLight.hollight.CONSTR_BOT"
  1831   "CONJ_SYM" > "HOL.conj_comms_1"
  1832   "CONJ_ASSOC" > "HOL.conj_assoc"
  1833   "CONJ_ACI" > "HOLLight.hollight.CONJ_ACI"
  1834   "COND_def" > "HOLLight.hollight.COND_def"
  1835   "COND_RATOR" > "HOLLight.hollight.COND_RATOR"
  1836   "COND_RAND" > "HOLLight.hollight.COND_RAND"
  1837   "COND_ID" > "HOLLight.hollight.COND_ID"
  1838   "COND_EXPAND" > "HOLLight.hollight.COND_EXPAND"
  1839   "COND_EQ_CLAUSE" > "HOLLight.hollight.COND_EQ_CLAUSE"
  1840   "COND_ELIM_THM" > "HOLLight.hollight.COND_ELIM_THM"
  1841   "COND_CLAUSES" > "HOLLight.hollight.COND_CLAUSES"
  1842   "COND_ABS" > "HOLLight.hollight.COND_ABS"
  1843   "COMPONENT" > "HOLLight.hollight.COMPONENT"
  1844   "CHOOSE_SUBSET" > "HOLLight.hollight.CHOOSE_SUBSET"
  1845   "CHOICE_def" > "HOLLight.hollight.CHOICE_def"
  1846   "CHOICE_DEF" > "HOLLight.hollight.CHOICE_DEF"
  1847   "CASEWISE_def" > "HOLLight.hollight.CASEWISE_def"
  1848   "CASEWISE_WORKS" > "HOLLight.hollight.CASEWISE_WORKS"
  1849   "CASEWISE_CASES" > "HOLLight.hollight.CASEWISE_CASES"
  1850   "CASEWISE" > "HOLLight.hollight.CASEWISE"
  1851   "CART_EQ" > "HOLLight.hollight.CART_EQ"
  1852   "CARD_def" > "HOLLight.hollight.CARD_def"
  1853   "CARD_UNION_LE" > "HOLLight.hollight.CARD_UNION_LE"
  1854   "CARD_UNION_EQ" > "HOLLight.hollight.CARD_UNION_EQ"
  1855   "CARD_UNIONS_LE" > "HOLLight.hollight.CARD_UNIONS_LE"
  1856   "CARD_UNION" > "HOLLight.hollight.CARD_UNION"
  1857   "CARD_SUBSET_LE" > "HOLLight.hollight.CARD_SUBSET_LE"
  1858   "CARD_SUBSET_EQ" > "HOLLight.hollight.CARD_SUBSET_EQ"
  1859   "CARD_SUBSET" > "HOLLight.hollight.CARD_SUBSET"
  1860   "CARD_PSUBSET" > "HOLLight.hollight.CARD_PSUBSET"
  1861   "CARD_PRODUCT" > "HOLLight.hollight.CARD_PRODUCT"
  1862   "CARD_POWERSET" > "HOLLight.hollight.CARD_POWERSET"
  1863   "CARD_NUMSEG_LT" > "HOLLight.hollight.CARD_NUMSEG_LT"
  1864   "CARD_NUMSEG_LEMMA" > "HOLLight.hollight.CARD_NUMSEG_LEMMA"
  1865   "CARD_NUMSEG_LE" > "HOLLight.hollight.CARD_NUMSEG_LE"
  1866   "CARD_NUMSEG_1" > "HOLLight.hollight.CARD_NUMSEG_1"
  1867   "CARD_NUMSEG" > "HOLLight.hollight.CARD_NUMSEG"
  1868   "CARD_LT_def" > "HOLLight.hollight.CARD_LT_def"
  1869   "CARD_LE_def" > "HOLLight.hollight.CARD_LE_def"
  1870   "CARD_LE_INJ" > "HOLLight.hollight.CARD_LE_INJ"
  1871   "CARD_IMAGE_LE" > "HOLLight.hollight.CARD_IMAGE_LE"
  1872   "CARD_IMAGE_INJ" > "HOLLight.hollight.CARD_IMAGE_INJ"
  1873   "CARD_GT_def" > "HOLLight.hollight.CARD_GT_def"
  1874   "CARD_GE_def" > "HOLLight.hollight.CARD_GE_def"
  1875   "CARD_GE_TRANS" > "HOLLight.hollight.CARD_GE_TRANS"
  1876   "CARD_GE_REFL" > "HOLLight.hollight.CARD_GE_REFL"
  1877   "CARD_FUNSPACE" > "HOLLight.hollight.CARD_FUNSPACE"
  1878   "CARD_FINITE_IMAGE" > "HOLLight.hollight.CARD_FINITE_IMAGE"
  1879   "CARD_EQ_def" > "HOLLight.hollight.CARD_EQ_def"
  1880   "CARD_EQ_SUM" > "HOLLight.hollight.CARD_EQ_SUM"
  1881   "CARD_EQ_NSUM" > "HOLLight.hollight.CARD_EQ_NSUM"
  1882   "CARD_EQ_0" > "HOLLight.hollight.CARD_EQ_0"
  1883   "CARD_DELETE" > "HOLLight.hollight.CARD_DELETE"
  1884   "CARD_CLAUSES" > "HOLLight.hollight.CARD_CLAUSES"
  1885   "BOUNDS_NOTZERO" > "HOLLight.hollight.BOUNDS_NOTZERO"
  1886   "BOUNDS_LINEAR_0" > "HOLLight.hollight.BOUNDS_LINEAR_0"
  1887   "BOUNDS_LINEAR" > "HOLLight.hollight.BOUNDS_LINEAR"
  1888   "BOUNDS_IGNORE" > "HOLLight.hollight.BOUNDS_IGNORE"
  1889   "BOUNDS_DIVIDED" > "HOLLight.hollight.BOUNDS_DIVIDED"
  1890   "BOTTOM_def" > "HOLLight.hollight.BOTTOM_def"
  1891   "BOOL_CASES_AX" > "Datatype.bool.nchotomy"
  1892   "BIT1_THM" > "HOLLightCompat.NUMERAL_BIT1_altdef"
  1893   "BIT0_THM" > "HOLLightCompat.NUMERAL_BIT0_def"
  1894   "BIJ_def" > "HOLLight.hollight.BIJ_def"
  1895   "BETA_THM" > "Presburger.fm_modd_pinf"
  1896   "ASSOC_def" > "HOLLight.hollight.ASSOC_def"
  1897   "ARITH_ZERO" > "HOLLight.hollight.ARITH_ZERO"
  1898   "ARITH_SUC" > "HOLLight.hollight.ARITH_SUC"
  1899   "ARITH_SUB" > "HOLLight.hollight.ARITH_SUB"
  1900   "ARITH_PRE" > "HOLLight.hollight.ARITH_PRE"
  1901   "ARITH_ODD" > "HOLLight.hollight.ARITH_ODD"
  1902   "ARITH_MULT" > "HOLLight.hollight.ARITH_MULT"
  1903   "ARITH_LT" > "HOLLight.hollight.ARITH_LT"
  1904   "ARITH_LE" > "HOLLight.hollight.ARITH_LE"
  1905   "ARITH_EXP" > "HOLLight.hollight.ARITH_EXP"
  1906   "ARITH_EVEN" > "HOLLight.hollight.ARITH_EVEN"
  1907   "ARITH_EQ" > "HOLLight.hollight.ARITH_EQ"
  1908   "ARITH_ADD" > "HOLLight.hollight.ARITH_ADD"
  1909   "APPEND_def" > "HOLLight.hollight.APPEND_def"
  1910   "APPEND_NIL" > "HOLLight.hollight.APPEND_NIL"
  1911   "APPEND_EQ_NIL" > "HOLLight.hollight.APPEND_EQ_NIL"
  1912   "APPEND_ASSOC" > "HOLLight.hollight.APPEND_ASSOC"
  1913   "AND_FORALL_THM" > "HOL.all_conj_distrib"
  1914   "AND_CLAUSES" > "HOLLight.hollight.AND_CLAUSES"
  1915   "AND_ALL2" > "HOLLight.hollight.AND_ALL2"
  1916   "AND_ALL" > "HOLLight.hollight.AND_ALL"
  1917   "ALL_list_def" > "HOLLight.hollight.ALL_list_def"
  1918   "ALL_T" > "HOLLight.hollight.ALL_T"
  1919   "ALL_MP" > "HOLLight.hollight.ALL_MP"
  1920   "ALL_MEM" > "HOLLight.hollight.ALL_MEM"
  1921   "ALL_MAP" > "HOLLight.hollight.ALL_MAP"
  1922   "ALL_IMP" > "HOLLight.hollight.ALL_IMP"
  1923   "ALL_APPEND" > "HOLLight.hollight.ALL_APPEND"
  1924   "ALL2_def" > "HOLLight.hollight.ALL2_def"
  1925   "ALL2_MAP2" > "HOLLight.hollight.ALL2_MAP2"
  1926   "ALL2_MAP" > "HOLLight.hollight.ALL2_MAP"
  1927   "ALL2_AND_RIGHT" > "HOLLight.hollight.ALL2_AND_RIGHT"
  1928   "ALL2_ALL" > "HOLLight.hollight.ALL2_ALL"
  1929   "ALL2" > "HOLLight.hollight.ALL2"
  1930   "ADMISSIBLE_SUM" > "HOLLight.hollight.ADMISSIBLE_SUM"
  1931   "ADMISSIBLE_NSUM" > "HOLLight.hollight.ADMISSIBLE_NSUM"
  1932   "ADMISSIBLE_NEST" > "HOLLight.hollight.ADMISSIBLE_NEST"
  1933   "ADMISSIBLE_LAMBDA" > "HOLLight.hollight.ADMISSIBLE_LAMBDA"
  1934   "ADMISSIBLE_IMP_SUPERADMISSIBLE" > "HOLLight.hollight.ADMISSIBLE_IMP_SUPERADMISSIBLE"
  1935   "ADMISSIBLE_CONST" > "HOLLight.hollight.ADMISSIBLE_CONST"
  1936   "ADMISSIBLE_COND" > "HOLLight.hollight.ADMISSIBLE_COND"
  1937   "ADMISSIBLE_COMB" > "HOLLight.hollight.ADMISSIBLE_COMB"
  1938   "ADMISSIBLE_BASE" > "HOLLight.hollight.ADMISSIBLE_BASE"
  1939   "ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
  1940   "ADD_SUC" > "Nat.add_Suc_right"
  1941   "ADD_SUBR2" > "Nat.diff_add_0"
  1942   "ADD_SUBR" > "HOLLight.hollight.ADD_SUBR"
  1943   "ADD_SUB2" > "Nat.diff_add_inverse"
  1944   "ADD_SUB" > "Nat.diff_add_inverse2"
  1945   "ADD_EQ_0" > "Nat.add_is_0"
  1946   "ADD_CLAUSES" > "HOLLight.hollight.ADD_CLAUSES"
  1947   "ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
  1948   "ADD_AC" > "HOLLight.hollight.ADD_AC"
  1949   "ADD_0" > "Presburger.add_right_zero"
  1950   "ADD1" > "HOLLight.hollight.ADD1"
  1951   "ABS_SIMP" > "Presburger.fm_modd_pinf"
  1952   "ABSORPTION" > "HOLLight.hollight.ABSORPTION"
  1953   ">_def" > "HOLLight.hollight.>_def"
  1954   ">=_def" > "HOLLight.hollight.>=_def"
  1955   "<_def" > "HOLLight.hollight.<_def"
  1956   "<=_def" > "HOLLight.hollight.<=_def"
  1957   "$_def" > "HOLLight.hollight.$_def"
  1958 
  1959 ignore_thms
  1960   "TYDEF_sum"
  1961   "TYDEF_prod"
  1962   "TYDEF_num"
  1963   "TYDEF_1"
  1964   "IND_SUC_0_EXISTS"
  1965   "DEF_one"
  1966   "DEF__0"
  1967   "DEF_SUC"
  1968   "DEF_NUM_REP"
  1969   "DEF_INR"
  1970   "DEF_INL"
  1971   "DEF_IND_SUC"
  1972   "DEF_IND_0"
  1973 
  1974 end