src/HOL/Import/HOL/prob_indep.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
  "indep_set" > "indep_set_primdef"
skalberg@14516
     7
  "indep" > "indep_primdef"
skalberg@14516
     8
  "alg_cover_set" > "alg_cover_set_primdef"
skalberg@14516
     9
  "alg_cover" > "alg_cover_primdef"
skalberg@14516
    10
skalberg@14516
    11
const_maps
skalberg@14516
    12
  "indep_set" > "HOL4Prob.prob_indep.indep_set"
skalberg@14516
    13
  "indep" > "HOL4Prob.prob_indep.indep"
skalberg@14516
    14
  "alg_cover_set" > "HOL4Prob.prob_indep.alg_cover_set"
skalberg@14516
    15
  "alg_cover" > "HOL4Prob.prob_indep.alg_cover"
skalberg@14516
    16
skalberg@14516
    17
thm_maps
skalberg@14516
    18
  "indep_set_primdef" > "HOL4Prob.prob_indep.indep_set_primdef"
skalberg@14516
    19
  "indep_set_def" > "HOL4Prob.prob_indep.indep_set_def"
skalberg@14516
    20
  "indep_primdef" > "HOL4Prob.prob_indep.indep_primdef"
skalberg@14516
    21
  "indep_def" > "HOL4Prob.prob_indep.indep_def"
skalberg@14516
    22
  "alg_cover_set_primdef" > "HOL4Prob.prob_indep.alg_cover_set_primdef"
skalberg@14516
    23
  "alg_cover_set_def" > "HOL4Prob.prob_indep.alg_cover_set_def"
skalberg@14516
    24
  "alg_cover_primdef" > "HOL4Prob.prob_indep.alg_cover_primdef"
skalberg@14516
    25
  "alg_cover_def" > "HOL4Prob.prob_indep.alg_cover_def"
skalberg@14516
    26
  "PROB_INDEP_BOUND" > "HOL4Prob.prob_indep.PROB_INDEP_BOUND"
skalberg@14516
    27
  "MAP_CONS_TL_FILTER" > "HOL4Prob.prob_indep.MAP_CONS_TL_FILTER"
skalberg@14516
    28
  "INDEP_UNIT" > "HOL4Prob.prob_indep.INDEP_UNIT"
skalberg@14516
    29
  "INDEP_SET_SYM" > "HOL4Prob.prob_indep.INDEP_SET_SYM"
skalberg@14516
    30
  "INDEP_SET_LIST" > "HOL4Prob.prob_indep.INDEP_SET_LIST"
skalberg@14516
    31
  "INDEP_SET_DISJOINT_DECOMP" > "HOL4Prob.prob_indep.INDEP_SET_DISJOINT_DECOMP"
skalberg@14516
    32
  "INDEP_SET_BASIC" > "HOL4Prob.prob_indep.INDEP_SET_BASIC"
skalberg@14516
    33
  "INDEP_SDEST" > "HOL4Prob.prob_indep.INDEP_SDEST"
skalberg@14516
    34
  "INDEP_PROB" > "HOL4Prob.prob_indep.INDEP_PROB"
skalberg@14516
    35
  "INDEP_MEASURABLE2" > "HOL4Prob.prob_indep.INDEP_MEASURABLE2"
skalberg@14516
    36
  "INDEP_MEASURABLE1" > "HOL4Prob.prob_indep.INDEP_MEASURABLE1"
skalberg@14516
    37
  "INDEP_INDEP_SET_LEMMA" > "HOL4Prob.prob_indep.INDEP_INDEP_SET_LEMMA"
skalberg@14516
    38
  "INDEP_INDEP_SET" > "HOL4Prob.prob_indep.INDEP_INDEP_SET"
skalberg@14516
    39
  "INDEP_BIND_SDEST" > "HOL4Prob.prob_indep.INDEP_BIND_SDEST"
skalberg@14516
    40
  "INDEP_BIND" > "HOL4Prob.prob_indep.INDEP_BIND"
skalberg@14516
    41
  "BIND_STEP" > "HOL4Prob.prob_indep.BIND_STEP"
skalberg@14516
    42
  "ALG_COVER_WELL_DEFINED" > "HOL4Prob.prob_indep.ALG_COVER_WELL_DEFINED"
skalberg@14516
    43
  "ALG_COVER_UNIV" > "HOL4Prob.prob_indep.ALG_COVER_UNIV"
skalberg@14516
    44
  "ALG_COVER_UNIQUE" > "HOL4Prob.prob_indep.ALG_COVER_UNIQUE"
skalberg@14516
    45
  "ALG_COVER_TAIL_STEP" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_STEP"
skalberg@14516
    46
  "ALG_COVER_TAIL_PROB" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_PROB"
skalberg@14516
    47
  "ALG_COVER_TAIL_MEASURABLE" > "HOL4Prob.prob_indep.ALG_COVER_TAIL_MEASURABLE"
skalberg@14516
    48
  "ALG_COVER_STEP" > "HOL4Prob.prob_indep.ALG_COVER_STEP"
skalberg@14516
    49
  "ALG_COVER_SET_INDUCTION" > "HOL4Prob.prob_indep.ALG_COVER_SET_INDUCTION"
skalberg@14516
    50
  "ALG_COVER_SET_CASES_THM" > "HOL4Prob.prob_indep.ALG_COVER_SET_CASES_THM"
skalberg@14516
    51
  "ALG_COVER_SET_CASES" > "HOL4Prob.prob_indep.ALG_COVER_SET_CASES"
skalberg@14516
    52
  "ALG_COVER_SET_BASIC" > "HOL4Prob.prob_indep.ALG_COVER_SET_BASIC"
skalberg@14516
    53
  "ALG_COVER_HEAD" > "HOL4Prob.prob_indep.ALG_COVER_HEAD"
skalberg@14516
    54
  "ALG_COVER_EXISTS_UNIQUE" > "HOL4Prob.prob_indep.ALG_COVER_EXISTS_UNIQUE"
skalberg@14516
    55
skalberg@14516
    56
end