|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"inf" > "inf_primdef"
|
|
|
7 |
|
|
|
8 |
const_maps
|
|
|
9 |
"inf" > "HOL4Prob.prob_extra.inf"
|
|
|
10 |
"COMPL" > "HOL4Base.pred_set.COMPL"
|
|
|
11 |
|
|
|
12 |
thm_maps
|
|
|
13 |
"inf_primdef" > "HOL4Prob.prob_extra.inf_primdef"
|
|
|
14 |
"inf_def" > "HOL4Prob.prob_extra.inf_def"
|
|
|
15 |
"X_HALF_HALF" > "HOL4Prob.prob_extra.X_HALF_HALF"
|
|
|
16 |
"UNION_DISJOINT_SPLIT" > "HOL4Prob.prob_extra.UNION_DISJOINT_SPLIT"
|
|
|
17 |
"UNION_DEF_ALT" > "HOL4Prob.prob_extra.UNION_DEF_ALT"
|
|
|
18 |
"SUBSET_EQ_DECOMP" > "HOL4Base.pred_set.SUBSET_ANTISYM"
|
|
|
19 |
"SUBSET_EQ" > "HOL4Prob.prob_extra.SUBSET_EQ"
|
|
|
20 |
"SET_EQ_EXT" > "HOL4Base.pred_set.EXTENSION"
|
|
|
21 |
"REAL_X_LE_SUP" > "HOL4Prob.prob_extra.REAL_X_LE_SUP"
|
|
|
22 |
"REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX"
|
|
|
23 |
"REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X"
|
|
|
24 |
"REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE"
|
|
|
25 |
"REAL_POW" > "RealPow.realpow_real_of_nat"
|
|
|
26 |
"REAL_LE_INV_LE" > "Ring_and_Field.le_imp_inverse_le"
|
|
|
27 |
"REAL_LE_EQ" > "Set.basic_trans_rules_26"
|
|
|
28 |
"REAL_INVINV_ALL" > "Ring_and_Field.inverse_inverse_eq"
|
|
|
29 |
"REAL_INF_MIN" > "HOL4Prob.prob_extra.REAL_INF_MIN"
|
|
|
30 |
"RAND_THM" > "HOL.arg_cong"
|
|
|
31 |
"POW_HALF_TWICE" > "HOL4Prob.prob_extra.POW_HALF_TWICE"
|
|
|
32 |
"POW_HALF_POS" > "HOL4Prob.prob_extra.POW_HALF_POS"
|
|
|
33 |
"POW_HALF_MONO" > "HOL4Prob.prob_extra.POW_HALF_MONO"
|
|
|
34 |
"POW_HALF_EXP" > "HOL4Prob.prob_extra.POW_HALF_EXP"
|
|
|
35 |
"ONE_MINUS_HALF" > "HOL4Prob.prob_extra.ONE_MINUS_HALF"
|
|
|
36 |
"MOD_TWO" > "HOL4Prob.prob_extra.MOD_TWO"
|
|
|
37 |
"MEM_NIL_MAP_CONS" > "HOL4Prob.prob_extra.MEM_NIL_MAP_CONS"
|
|
|
38 |
"MEM_NIL" > "HOL4Prob.prob_extra.MEM_NIL"
|
|
|
39 |
"MEM_FILTER" > "HOL4Prob.prob_extra.MEM_FILTER"
|
|
|
40 |
"MAP_MEM" > "HOL4Prob.prob_extra.MAP_MEM"
|
|
|
41 |
"MAP_ID" > "List.map_ident"
|
|
15647
|
42 |
"LENGTH_FILTER" > "List.length_filter_le"
|
|
14516
|
43 |
"LAST_MEM" > "HOL4Prob.prob_extra.LAST_MEM"
|
|
|
44 |
"LAST_MAP_CONS" > "HOL4Prob.prob_extra.LAST_MAP_CONS"
|
|
|
45 |
"IS_PREFIX_TRANS" > "HOL4Prob.prob_extra.IS_PREFIX_TRANS"
|
|
|
46 |
"IS_PREFIX_SNOC" > "HOL4Prob.prob_extra.IS_PREFIX_SNOC"
|
|
|
47 |
"IS_PREFIX_REFL" > "HOL4Prob.prob_extra.IS_PREFIX_REFL"
|
|
|
48 |
"IS_PREFIX_NIL" > "HOL4Prob.prob_extra.IS_PREFIX_NIL"
|
|
|
49 |
"IS_PREFIX_LENGTH_ANTI" > "HOL4Prob.prob_extra.IS_PREFIX_LENGTH_ANTI"
|
|
|
50 |
"IS_PREFIX_LENGTH" > "HOL4Prob.prob_extra.IS_PREFIX_LENGTH"
|
|
|
51 |
"IS_PREFIX_BUTLAST" > "HOL4Prob.prob_extra.IS_PREFIX_BUTLAST"
|
|
|
52 |
"IS_PREFIX_ANTISYM" > "HOL4Prob.prob_extra.IS_PREFIX_ANTISYM"
|
|
|
53 |
"IN_EMPTY" > "HOL4Base.pred_set.NOT_IN_EMPTY"
|
|
|
54 |
"IN_COMPL" > "HOL4Base.pred_set.IN_COMPL"
|
|
|
55 |
"INV_SUC_POS" > "HOL4Prob.prob_extra.INV_SUC_POS"
|
|
|
56 |
"INV_SUC_MAX" > "HOL4Prob.prob_extra.INV_SUC_MAX"
|
|
|
57 |
"INV_SUC" > "HOL4Prob.prob_extra.INV_SUC"
|
|
|
58 |
"INTER_UNION_RDISTRIB" > "HOL4Prob.prob_extra.INTER_UNION_RDISTRIB"
|
|
|
59 |
"INTER_UNION_COMPL" > "HOL4Base.pred_set.INTER_UNION_COMPL"
|
|
|
60 |
"INTER_IS_EMPTY" > "HOL4Prob.prob_extra.INTER_IS_EMPTY"
|
|
|
61 |
"INF_DEF_ALT" > "HOL4Prob.prob_extra.INF_DEF_ALT"
|
|
|
62 |
"HALF_POS" > "HOL4Prob.prob_extra.HALF_POS"
|
|
|
63 |
"HALF_LT_1" > "HOL4Prob.prob_extra.HALF_LT_1"
|
|
|
64 |
"HALF_CANCEL" > "HOL4Prob.prob_extra.HALF_CANCEL"
|
|
|
65 |
"GSPEC_DEF_ALT" > "HOL4Prob.prob_extra.GSPEC_DEF_ALT"
|
|
|
66 |
"FOLDR_MAP" > "HOL4Prob.prob_extra.FOLDR_MAP"
|
|
|
67 |
"FILTER_TRUE" > "HOL4Prob.prob_extra.FILTER_TRUE"
|
|
|
68 |
"FILTER_OUT_ELT" > "HOL4Prob.prob_extra.FILTER_OUT_ELT"
|
|
|
69 |
"FILTER_MEM" > "HOL4Prob.prob_extra.FILTER_MEM"
|
|
|
70 |
"FILTER_FALSE" > "HOL4Prob.prob_extra.FILTER_FALSE"
|
|
|
71 |
"EXP_DIV_TWO" > "HOL4Prob.prob_extra.EXP_DIV_TWO"
|
|
|
72 |
"EXISTS_LONGEST" > "HOL4Prob.prob_extra.EXISTS_LONGEST"
|
|
|
73 |
"EVEN_ODD_EXISTS_EQ" > "HOL4Prob.prob_extra.EVEN_ODD_EXISTS_EQ"
|
|
|
74 |
"EVEN_ODD_BASIC" > "HOL4Prob.prob_extra.EVEN_ODD_BASIC"
|
|
|
75 |
"EVEN_EXP_TWO" > "HOL4Prob.prob_extra.EVEN_EXP_TWO"
|
|
|
76 |
"EQ_EXT_EQ" > "Fun.expand_fun_eq"
|
|
|
77 |
"DIV_TWO_UNIQUE" > "HOL4Prob.prob_extra.DIV_TWO_UNIQUE"
|
|
|
78 |
"DIV_TWO_MONO_EVEN" > "HOL4Prob.prob_extra.DIV_TWO_MONO_EVEN"
|
|
|
79 |
"DIV_TWO_MONO" > "HOL4Prob.prob_extra.DIV_TWO_MONO"
|
|
|
80 |
"DIV_TWO_EXP" > "HOL4Prob.prob_extra.DIV_TWO_EXP"
|
|
|
81 |
"DIV_TWO_CANCEL" > "HOL4Prob.prob_extra.DIV_TWO_CANCEL"
|
|
|
82 |
"DIV_TWO_BASIC" > "HOL4Prob.prob_extra.DIV_TWO_BASIC"
|
|
|
83 |
"DIV_TWO" > "HOL4Prob.prob_extra.DIV_TWO"
|
|
|
84 |
"DIV_THEN_MULT" > "HOL4Prob.prob_extra.DIV_THEN_MULT"
|
|
|
85 |
"DIVISION_TWO" > "HOL4Prob.prob_extra.DIVISION_TWO"
|
|
|
86 |
"COMPL_def" > "HOL4Base.pred_set.COMPL_DEF"
|
|
|
87 |
"COMPL_SPLITS" > "HOL4Base.pred_set.COMPL_SPLITS"
|
|
|
88 |
"COMPL_COMPL" > "HOL4Base.pred_set.COMPL_COMPL"
|
|
|
89 |
"COMPL_CLAUSES" > "HOL4Base.pred_set.COMPL_CLAUSES"
|
|
|
90 |
"BOOL_BOOL_CASES_THM" > "HOL4Prob.prob_extra.BOOL_BOOL_CASES_THM"
|
|
|
91 |
"BOOL_BOOL_CASES" > "HOL4Base.bool.BOOL_FUN_INDUCT"
|
|
|
92 |
"APPEND_MEM" > "HOL4Base.list.MEM_APPEND"
|
|
|
93 |
"ABS_UNIT_INTERVAL" > "HOL4Prob.prob_extra.ABS_UNIT_INTERVAL"
|
|
|
94 |
"ABS_BETWEEN_LE" > "HOL4Prob.prob_extra.ABS_BETWEEN_LE"
|
|
|
95 |
|
|
|
96 |
end
|