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