|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"prob" > "prob_primdef"
|
|
|
7 |
"algebra_measure" > "algebra_measure_primdef"
|
|
|
8 |
"alg_measure" > "alg_measure_primdef"
|
|
|
9 |
|
|
|
10 |
const_maps
|
|
|
11 |
"prob" > "HOL4Prob.prob.prob"
|
|
|
12 |
"algebra_measure" > "HOL4Prob.prob.algebra_measure"
|
|
|
13 |
|
|
|
14 |
thm_maps
|
|
|
15 |
"prob_primdef" > "HOL4Prob.prob.prob_primdef"
|
|
|
16 |
"prob_def" > "HOL4Prob.prob.prob_def"
|
|
|
17 |
"algebra_measure_primdef" > "HOL4Prob.prob.algebra_measure_primdef"
|
|
|
18 |
"algebra_measure_def" > "HOL4Prob.prob.algebra_measure_def"
|
|
|
19 |
"alg_measure_def" > "HOL4Prob.prob.alg_measure_def"
|
|
|
20 |
"X_LE_PROB" > "HOL4Prob.prob.X_LE_PROB"
|
|
|
21 |
"PROB_SUP_EXISTS2" > "HOL4Prob.prob.PROB_SUP_EXISTS2"
|
|
|
22 |
"PROB_SUP_EXISTS1" > "HOL4Prob.prob.PROB_SUP_EXISTS1"
|
|
|
23 |
"PROB_SUBSET_MONO" > "HOL4Prob.prob.PROB_SUBSET_MONO"
|
|
|
24 |
"PROB_STL" > "HOL4Prob.prob.PROB_STL"
|
|
|
25 |
"PROB_SHD" > "HOL4Prob.prob.PROB_SHD"
|
|
|
26 |
"PROB_SDROP" > "HOL4Prob.prob.PROB_SDROP"
|
|
|
27 |
"PROB_RANGE" > "HOL4Prob.prob.PROB_RANGE"
|
|
|
28 |
"PROB_POS" > "HOL4Prob.prob.PROB_POS"
|
|
|
29 |
"PROB_MAX" > "HOL4Prob.prob.PROB_MAX"
|
|
|
30 |
"PROB_LE_X" > "HOL4Prob.prob.PROB_LE_X"
|
|
|
31 |
"PROB_INTER_SHD" > "HOL4Prob.prob.PROB_INTER_SHD"
|
|
|
32 |
"PROB_INTER_HALVES" > "HOL4Prob.prob.PROB_INTER_HALVES"
|
|
|
33 |
"PROB_COMPL_LE1" > "HOL4Prob.prob.PROB_COMPL_LE1"
|
|
|
34 |
"PROB_COMPL" > "HOL4Prob.prob.PROB_COMPL"
|
|
|
35 |
"PROB_BASIC" > "HOL4Prob.prob.PROB_BASIC"
|
|
|
36 |
"PROB_ALGEBRA" > "HOL4Prob.prob.PROB_ALGEBRA"
|
|
|
37 |
"PROB_ALG" > "HOL4Prob.prob.PROB_ALG"
|
|
|
38 |
"PROB_ADDITIVE" > "HOL4Prob.prob.PROB_ADDITIVE"
|
|
|
39 |
"ALG_TWINS_MEASURE" > "HOL4Prob.prob.ALG_TWINS_MEASURE"
|
|
|
40 |
"ALG_MEASURE_TLS" > "HOL4Prob.prob.ALG_MEASURE_TLS"
|
|
|
41 |
"ALG_MEASURE_POS" > "HOL4Prob.prob.ALG_MEASURE_POS"
|
|
|
42 |
"ALG_MEASURE_COMPL" > "HOL4Prob.prob.ALG_MEASURE_COMPL"
|
|
|
43 |
"ALG_MEASURE_BASIC" > "HOL4Prob.prob.ALG_MEASURE_BASIC"
|
|
|
44 |
"ALG_MEASURE_APPEND" > "HOL4Prob.prob.ALG_MEASURE_APPEND"
|
|
|
45 |
"ALG_MEASURE_ADDITIVE" > "HOL4Prob.prob.ALG_MEASURE_ADDITIVE"
|
|
|
46 |
"ALG_CANON_PREFS_MONO" > "HOL4Prob.prob.ALG_CANON_PREFS_MONO"
|
|
|
47 |
"ALG_CANON_MONO" > "HOL4Prob.prob.ALG_CANON_MONO"
|
|
|
48 |
"ALG_CANON_MERGE_MONO" > "HOL4Prob.prob.ALG_CANON_MERGE_MONO"
|
|
|
49 |
"ALG_CANON_FIND_MONO" > "HOL4Prob.prob.ALG_CANON_FIND_MONO"
|
|
|
50 |
"ALG_CANON2_MONO" > "HOL4Prob.prob.ALG_CANON2_MONO"
|
|
|
51 |
"ALG_CANON1_MONO" > "HOL4Prob.prob.ALG_CANON1_MONO"
|
|
|
52 |
"ALGEBRA_MEASURE_RANGE" > "HOL4Prob.prob.ALGEBRA_MEASURE_RANGE"
|
|
|
53 |
"ALGEBRA_MEASURE_POS" > "HOL4Prob.prob.ALGEBRA_MEASURE_POS"
|
|
|
54 |
"ALGEBRA_MEASURE_MONO_EMBED" > "HOL4Prob.prob.ALGEBRA_MEASURE_MONO_EMBED"
|
|
|
55 |
"ALGEBRA_MEASURE_MAX" > "HOL4Prob.prob.ALGEBRA_MEASURE_MAX"
|
|
|
56 |
"ALGEBRA_MEASURE_DEF_ALT" > "HOL4Prob.prob.ALGEBRA_MEASURE_DEF_ALT"
|
|
|
57 |
"ALGEBRA_MEASURE_BASIC" > "HOL4Prob.prob.ALGEBRA_MEASURE_BASIC"
|
|
|
58 |
"ALGEBRA_CANON_MEASURE_MAX" > "HOL4Prob.prob.ALGEBRA_CANON_MEASURE_MAX"
|
|
|
59 |
"ABS_PROB" > "HOL4Prob.prob.ABS_PROB"
|
|
|
60 |
|
|
|
61 |
end
|