|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"uniform_tupled" > "uniform_tupled_def"
|
|
|
7 |
"uniform" > "uniform_primdef"
|
|
|
8 |
"unif_tupled" > "unif_tupled_def"
|
|
|
9 |
"unif_bound" > "unif_bound_primdef"
|
|
|
10 |
"unif" > "unif_primdef"
|
|
|
11 |
|
|
|
12 |
const_maps
|
|
|
13 |
"uniform_tupled" > "HOL4Prob.prob_uniform.uniform_tupled"
|
|
|
14 |
"uniform" > "HOL4Prob.prob_uniform.uniform"
|
|
|
15 |
"unif_tupled" > "HOL4Prob.prob_uniform.unif_tupled"
|
|
|
16 |
"unif_bound" > "HOL4Prob.prob_uniform.unif_bound"
|
|
|
17 |
"unif" > "HOL4Prob.prob_uniform.unif"
|
|
|
18 |
|
|
|
19 |
thm_maps
|
|
|
20 |
"uniform_tupled_primitive_def" > "HOL4Prob.prob_uniform.uniform_tupled_primitive_def"
|
|
|
21 |
"uniform_tupled_def" > "HOL4Prob.prob_uniform.uniform_tupled_def"
|
|
|
22 |
"uniform_primdef" > "HOL4Prob.prob_uniform.uniform_primdef"
|
|
|
23 |
"uniform_ind" > "HOL4Prob.prob_uniform.uniform_ind"
|
|
|
24 |
"uniform_def" > "HOL4Prob.prob_uniform.uniform_def"
|
|
|
25 |
"uniform_curried_def" > "HOL4Prob.prob_uniform.uniform_curried_def"
|
|
|
26 |
"unif_tupled_primitive_def" > "HOL4Prob.prob_uniform.unif_tupled_primitive_def"
|
|
|
27 |
"unif_tupled_def" > "HOL4Prob.prob_uniform.unif_tupled_def"
|
|
|
28 |
"unif_primdef" > "HOL4Prob.prob_uniform.unif_primdef"
|
|
|
29 |
"unif_ind" > "HOL4Prob.prob_uniform.unif_ind"
|
|
|
30 |
"unif_def" > "HOL4Prob.prob_uniform.unif_def"
|
|
|
31 |
"unif_curried_def" > "HOL4Prob.prob_uniform.unif_curried_def"
|
|
|
32 |
"unif_bound_primitive_def" > "HOL4Prob.prob_uniform.unif_bound_primitive_def"
|
|
|
33 |
"unif_bound_primdef" > "HOL4Prob.prob_uniform.unif_bound_primdef"
|
|
|
34 |
"unif_bound_ind" > "HOL4Prob.prob_uniform.unif_bound_ind"
|
|
|
35 |
"unif_bound_def" > "HOL4Prob.prob_uniform.unif_bound_def"
|
|
|
36 |
"UNIF_RANGE" > "HOL4Prob.prob_uniform.UNIF_RANGE"
|
|
|
37 |
"UNIF_DEF_MONAD" > "HOL4Prob.prob_uniform.UNIF_DEF_MONAD"
|
|
|
38 |
"UNIF_BOUND_UPPER_SUC" > "HOL4Prob.prob_uniform.UNIF_BOUND_UPPER_SUC"
|
|
|
39 |
"UNIF_BOUND_UPPER" > "HOL4Prob.prob_uniform.UNIF_BOUND_UPPER"
|
|
|
40 |
"UNIF_BOUND_LOWER_SUC" > "HOL4Prob.prob_uniform.UNIF_BOUND_LOWER_SUC"
|
|
|
41 |
"UNIF_BOUND_LOWER" > "HOL4Prob.prob_uniform.UNIF_BOUND_LOWER"
|
|
|
42 |
"UNIFORM_RANGE" > "HOL4Prob.prob_uniform.UNIFORM_RANGE"
|
|
|
43 |
"UNIFORM_DEF_MONAD" > "HOL4Prob.prob_uniform.UNIFORM_DEF_MONAD"
|
|
|
44 |
"SUC_DIV_TWO_ZERO" > "HOL4Prob.prob_uniform.SUC_DIV_TWO_ZERO"
|
|
|
45 |
"PROB_UNIF_PAIR" > "HOL4Prob.prob_uniform.PROB_UNIF_PAIR"
|
|
|
46 |
"PROB_UNIF_GOOD" > "HOL4Prob.prob_uniform.PROB_UNIF_GOOD"
|
|
|
47 |
"PROB_UNIF_BOUND" > "HOL4Prob.prob_uniform.PROB_UNIF_BOUND"
|
|
|
48 |
"PROB_UNIFORM_UPPER_BOUND" > "HOL4Prob.prob_uniform.PROB_UNIFORM_UPPER_BOUND"
|
|
|
49 |
"PROB_UNIFORM_SUC" > "HOL4Prob.prob_uniform.PROB_UNIFORM_SUC"
|
|
|
50 |
"PROB_UNIFORM_PAIR_SUC" > "HOL4Prob.prob_uniform.PROB_UNIFORM_PAIR_SUC"
|
|
|
51 |
"PROB_UNIFORM_LOWER_BOUND" > "HOL4Prob.prob_uniform.PROB_UNIFORM_LOWER_BOUND"
|
|
|
52 |
"PROB_UNIFORM" > "HOL4Prob.prob_uniform.PROB_UNIFORM"
|
|
|
53 |
"PROB_UNIF" > "HOL4Prob.prob_uniform.PROB_UNIF"
|
|
|
54 |
"INDEP_UNIFORM" > "HOL4Prob.prob_uniform.INDEP_UNIFORM"
|
|
|
55 |
"INDEP_UNIF" > "HOL4Prob.prob_uniform.INDEP_UNIF"
|
|
|
56 |
|
|
|
57 |
end
|