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