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
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "measurable" > "measurable_primdef"
     7   "algebra_embed" > "algebra_embed_primdef"
     8   "alg_embed" > "alg_embed_primdef"
     9 
    10 const_maps
    11   "measurable" > "HOL4Prob.prob_algebra.measurable"
    12 
    13 thm_maps
    14   "measurable_primdef" > "HOL4Prob.prob_algebra.measurable_primdef"
    15   "measurable_def" > "HOL4Prob.prob_algebra.measurable_def"
    16   "algebra_embed_def" > "HOL4Prob.prob_algebra.algebra_embed_def"
    17   "alg_embed_def" > "HOL4Prob.prob_algebra.alg_embed_def"
    18   "MEASURABLE_UNION" > "HOL4Prob.prob_algebra.MEASURABLE_UNION"
    19   "MEASURABLE_STL" > "HOL4Prob.prob_algebra.MEASURABLE_STL"
    20   "MEASURABLE_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_SHD"
    21   "MEASURABLE_SDROP" > "HOL4Prob.prob_algebra.MEASURABLE_SDROP"
    22   "MEASURABLE_INTER_SHD" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_SHD"
    23   "MEASURABLE_INTER_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_INTER_HALVES"
    24   "MEASURABLE_INTER" > "HOL4Prob.prob_algebra.MEASURABLE_INTER"
    25   "MEASURABLE_HALVES" > "HOL4Prob.prob_algebra.MEASURABLE_HALVES"
    26   "MEASURABLE_COMPL" > "HOL4Prob.prob_algebra.MEASURABLE_COMPL"
    27   "MEASURABLE_BASIC" > "HOL4Prob.prob_algebra.MEASURABLE_BASIC"
    28   "MEASURABLE_ALGEBRA" > "HOL4Prob.prob_algebra.MEASURABLE_ALGEBRA"
    29   "INTER_STL" > "HOL4Prob.prob_algebra.INTER_STL"
    30   "HALVES_INTER" > "HOL4Prob.prob_algebra.HALVES_INTER"
    31   "COMPL_SHD" > "HOL4Prob.prob_algebra.COMPL_SHD"
    32   "ALG_EMBED_TWINS" > "HOL4Prob.prob_algebra.ALG_EMBED_TWINS"
    33   "ALG_EMBED_PREFIX_SUBSET" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX_SUBSET"
    34   "ALG_EMBED_PREFIX" > "HOL4Prob.prob_algebra.ALG_EMBED_PREFIX"
    35   "ALG_EMBED_POPULATED" > "HOL4Prob.prob_algebra.ALG_EMBED_POPULATED"
    36   "ALG_EMBED_NIL" > "HOL4Prob.prob_algebra.ALG_EMBED_NIL"
    37   "ALG_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALG_EMBED_BASIC"
    38   "ALG_CANON_REP" > "HOL4Prob.prob_algebra.ALG_CANON_REP"
    39   "ALG_CANON_PREFS_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_PREFS_EMBED"
    40   "ALG_CANON_MERGE_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_MERGE_EMBED"
    41   "ALG_CANON_FIND_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_FIND_EMBED"
    42   "ALG_CANON_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON_EMBED"
    43   "ALG_CANON2_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON2_EMBED"
    44   "ALG_CANON1_EMBED" > "HOL4Prob.prob_algebra.ALG_CANON1_EMBED"
    45   "ALGEBRA_EMBED_TLS" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_TLS"
    46   "ALGEBRA_EMBED_MEM" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_MEM"
    47   "ALGEBRA_EMBED_COMPL" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_COMPL"
    48   "ALGEBRA_EMBED_BASIC" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_BASIC"
    49   "ALGEBRA_EMBED_APPEND" > "HOL4Prob.prob_algebra.ALGEBRA_EMBED_APPEND"
    50   "ALGEBRA_CANON_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_UNIV"
    51   "ALGEBRA_CANON_EMBED_UNIV" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_UNIV"
    52   "ALGEBRA_CANON_EMBED_EMPTY" > "HOL4Prob.prob_algebra.ALGEBRA_CANON_EMBED_EMPTY"
    53 
    54 end