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