21 "REAL_X_LE_SUP" > "HOL4Prob.prob_extra.REAL_X_LE_SUP" |
21 "REAL_X_LE_SUP" > "HOL4Prob.prob_extra.REAL_X_LE_SUP" |
22 "REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX" |
22 "REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX" |
23 "REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X" |
23 "REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X" |
24 "REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE" |
24 "REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE" |
25 "REAL_POW" > "RealPow.realpow_real_of_nat" |
25 "REAL_POW" > "RealPow.realpow_real_of_nat" |
26 "REAL_LE_INV_LE" > "Ring_and_Field.le_imp_inverse_le" |
26 "REAL_LE_INV_LE" > "Rings.le_imp_inverse_le" |
27 "REAL_LE_EQ" > "Set.basic_trans_rules_26" |
27 "REAL_LE_EQ" > "Set.basic_trans_rules_26" |
28 "REAL_INVINV_ALL" > "Ring_and_Field.inverse_inverse_eq" |
28 "REAL_INVINV_ALL" > "Rings.inverse_inverse_eq" |
29 "REAL_INF_MIN" > "HOL4Prob.prob_extra.REAL_INF_MIN" |
29 "REAL_INF_MIN" > "HOL4Prob.prob_extra.REAL_INF_MIN" |
30 "RAND_THM" > "HOL.arg_cong" |
30 "RAND_THM" > "HOL.arg_cong" |
31 "POW_HALF_TWICE" > "HOL4Prob.prob_extra.POW_HALF_TWICE" |
31 "POW_HALF_TWICE" > "HOL4Prob.prob_extra.POW_HALF_TWICE" |
32 "POW_HALF_POS" > "HOL4Prob.prob_extra.POW_HALF_POS" |
32 "POW_HALF_POS" > "HOL4Prob.prob_extra.POW_HALF_POS" |
33 "POW_HALF_MONO" > "HOL4Prob.prob_extra.POW_HALF_MONO" |
33 "POW_HALF_MONO" > "HOL4Prob.prob_extra.POW_HALF_MONO" |