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
     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