|
14516
|
1 |
import
|
|
|
2 |
|
|
|
3 |
import_segment "hol4"
|
|
|
4 |
|
|
|
5 |
def_maps
|
|
|
6 |
"measurable" > "measurable_primdef"
|
|
|
7 |
"algebra_embed" > "algebra_embed_primdef"
|
|
|
8 |
"alg_embed" > "alg_embed_primdef"
|
|
|
9 |
|
|
|
10 |
const_maps
|
|
|
11 |
"measurable" > "HOL4Prob.prob_algebra.measurable"
|
|
|
12 |
|
|
|
13 |
thm_maps
|
|
|
14 |
"measurable_primdef" > "HOL4Prob.prob_algebra.measurable_primdef"
|
|
|
15 |
"measurable_def" > "HOL4Prob.prob_algebra.measurable_def"
|
|
|
16 |
"algebra_embed_def" > "HOL4Prob.prob_algebra.algebra_embed_def"
|
|
|
17 |
"alg_embed_def" > "HOL4Prob.prob_algebra.alg_embed_def"
|
|
|
18 |
"MEASURABLE_UNION" > "HOL4Prob.prob_algebra.MEASURABLE_UNION"
|
|
|
19 |
"MEASURABLE_STL" > "HOL4Prob.prob_algebra.MEASURABLE_STL"
|
|
|
20 |
"MEASURABLE_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_SHD"
|
|
|
21 |
"MEASURABLE_SDROP" > "HOL4Prob.prob_algebra.MEASURABLE_SDROP"
|
|
|
22 |
"MEASURABLE_INTER_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_SHD"
|
|
|
23 |
"MEASURABLE_INTER_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_HALVES"
|
|
|
24 |
"MEASURABLE_INTER" > "HOL4Prob.prob_algebra.MEASURABLE_INTER"
|
|
|
25 |
"MEASURABLE_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_HALVES"
|
|
|
26 |
"MEASURABLE_COMPL" > "HOL4Prob.prob_algebra.MEASURABLE_COMPL"
|
|
|
27 |
"MEASURABLE_BASIC" > "HOL4Prob.prob_algebra.MEASURABLE_BASIC"
|
|
|
28 |
"MEASURABLE_ALGEBRA" > "HOL4Prob.prob_algebra.MEASURABLE_ALGEBRA"
|
|
|
29 |
"INTER_STL" > "HOL4Prob.prob_algebra.INTER_STL"
|
|
|
30 |
"HALVES_INTER" > "HOL4Prob.prob_algebra.HALVES_INTER"
|
|
|
31 |
"COMPL_SHD" > "HOL4Prob.prob_algebra.COMPL_SHD"
|
|
|
32 |
"ALG_EMBED_TWINS" > "HOL4Prob.prob_algebra.ALG_EMBED_TWINS"
|
|
|
33 |
"ALG_EMBED_PREFIX_SUBSET" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX_SUBSET"
|
|
|
34 |
"ALG_EMBED_PREFIX" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX"
|
|
|
35 |
"ALG_EMBED_POPULATED" > "HOL4Prob.prob_algebra.ALG_EMBED_POPULATED"
|
|
|
36 |
"ALG_EMBED_NIL" > "HOL4Prob.prob_algebra.ALG_EMBED_NIL"
|
|
|
37 |
"ALG_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALG_EMBED_BASIC"
|
|
|
38 |
"ALG_CANON_REP" > "HOL4Prob.prob_algebra.ALG_CANON_REP"
|
|
|
39 |
"ALG_CANON_PREFS_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_PREFS_EMBED"
|
|
|
40 |
"ALG_CANON_MERGE_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_MERGE_EMBED"
|
|
|
41 |
"ALG_CANON_FIND_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_FIND_EMBED"
|
|
|
42 |
"ALG_CANON_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_EMBED"
|
|
|
43 |
"ALG_CANON2_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON2_EMBED"
|
|
|
44 |
"ALG_CANON1_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON1_EMBED"
|
|
|
45 |
"ALGEBRA_EMBED_TLS" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_TLS"
|
|
|
46 |
"ALGEBRA_EMBED_MEM" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_MEM"
|
|
|
47 |
"ALGEBRA_EMBED_COMPL" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_COMPL"
|
|
|
48 |
"ALGEBRA_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_BASIC"
|
|
|
49 |
"ALGEBRA_EMBED_APPEND" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_APPEND"
|
|
|
50 |
"ALGEBRA_CANON_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_UNIV"
|
|
|
51 |
"ALGEBRA_CANON_EMBED_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_UNIV"
|
|
|
52 |
"ALGEBRA_CANON_EMBED_EMPTY" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_EMPTY"
|
|
|
53 |
|
|
|
54 |
end
|