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