src/HOL/Import/HOL/prob_algebra.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
permissions -rw-r--r--
adaptions to codegen_package
skalberg@14516
     1
import
skalberg@14516
     2
skalberg@14516
     3
import_segment "hol4"
skalberg@14516
     4
skalberg@14516
     5
def_maps
skalberg@14516
     6
  "measurable" > "measurable_primdef"
skalberg@14516
     7
  "algebra_embed" > "algebra_embed_primdef"
skalberg@14516
     8
  "alg_embed" > "alg_embed_primdef"
skalberg@14516
     9
skalberg@14516
    10
const_maps
skalberg@14516
    11
  "measurable" > "HOL4Prob.prob_algebra.measurable"
skalberg@14516
    12
skalberg@14516
    13
thm_maps
skalberg@14516
    14
  "measurable_primdef" > "HOL4Prob.prob_algebra.measurable_primdef"
skalberg@14516
    15
  "measurable_def" > "HOL4Prob.prob_algebra.measurable_def"
skalberg@14516
    16
  "algebra_embed_def" > "HOL4Prob.prob_algebra.algebra_embed_def"
skalberg@14516
    17
  "alg_embed_def" > "HOL4Prob.prob_algebra.alg_embed_def"
skalberg@14516
    18
  "MEASURABLE_UNION" > "HOL4Prob.prob_algebra.MEASURABLE_UNION"
skalberg@14516
    19
  "MEASURABLE_STL" > "HOL4Prob.prob_algebra.MEASURABLE_STL"
skalberg@14516
    20
  "MEASURABLE_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_SHD"
skalberg@14516
    21
  "MEASURABLE_SDROP" > "HOL4Prob.prob_algebra.MEASURABLE_SDROP"
skalberg@14516
    22
  "MEASURABLE_INTER_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_SHD"
skalberg@14516
    23
  "MEASURABLE_INTER_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_HALVES"
skalberg@14516
    24
  "MEASURABLE_INTER" > "HOL4Prob.prob_algebra.MEASURABLE_INTER"
skalberg@14516
    25
  "MEASURABLE_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_HALVES"
skalberg@14516
    26
  "MEASURABLE_COMPL" > "HOL4Prob.prob_algebra.MEASURABLE_COMPL"
skalberg@14516
    27
  "MEASURABLE_BASIC" > "HOL4Prob.prob_algebra.MEASURABLE_BASIC"
skalberg@14516
    28
  "MEASURABLE_ALGEBRA" > "HOL4Prob.prob_algebra.MEASURABLE_ALGEBRA"
skalberg@14516
    29
  "INTER_STL" > "HOL4Prob.prob_algebra.INTER_STL"
skalberg@14516
    30
  "HALVES_INTER" > "HOL4Prob.prob_algebra.HALVES_INTER"
skalberg@14516
    31
  "COMPL_SHD" > "HOL4Prob.prob_algebra.COMPL_SHD"
skalberg@14516
    32
  "ALG_EMBED_TWINS" > "HOL4Prob.prob_algebra.ALG_EMBED_TWINS"
skalberg@14516
    33
  "ALG_EMBED_PREFIX_SUBSET" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX_SUBSET"
skalberg@14516
    34
  "ALG_EMBED_PREFIX" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX"
skalberg@14516
    35
  "ALG_EMBED_POPULATED" > "HOL4Prob.prob_algebra.ALG_EMBED_POPULATED"
skalberg@14516
    36
  "ALG_EMBED_NIL" > "HOL4Prob.prob_algebra.ALG_EMBED_NIL"
skalberg@14516
    37
  "ALG_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALG_EMBED_BASIC"
skalberg@14516
    38
  "ALG_CANON_REP" > "HOL4Prob.prob_algebra.ALG_CANON_REP"
skalberg@14516
    39
  "ALG_CANON_PREFS_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_PREFS_EMBED"
skalberg@14516
    40
  "ALG_CANON_MERGE_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_MERGE_EMBED"
skalberg@14516
    41
  "ALG_CANON_FIND_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_FIND_EMBED"
skalberg@14516
    42
  "ALG_CANON_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_EMBED"
skalberg@14516
    43
  "ALG_CANON2_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON2_EMBED"
skalberg@14516
    44
  "ALG_CANON1_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON1_EMBED"
skalberg@14516
    45
  "ALGEBRA_EMBED_TLS" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_TLS"
skalberg@14516
    46
  "ALGEBRA_EMBED_MEM" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_MEM"
skalberg@14516
    47
  "ALGEBRA_EMBED_COMPL" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_COMPL"
skalberg@14516
    48
  "ALGEBRA_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_BASIC"
skalberg@14516
    49
  "ALGEBRA_EMBED_APPEND" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_APPEND"
skalberg@14516
    50
  "ALGEBRA_CANON_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_UNIV"
skalberg@14516
    51
  "ALGEBRA_CANON_EMBED_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_UNIV"
skalberg@14516
    52
  "ALGEBRA_CANON_EMBED_EMPTY" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_EMPTY"
skalberg@14516
    53
skalberg@14516
    54
end