src/HOL/Import/HOL/prob_extra.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 15647 b1f486a9c56b
child 35050 9f841f20dca6
permissions -rw-r--r--
adaptions to codegen_package
     1 import
     2 
     3 import_segment "hol4"
     4 
     5 def_maps
     6   "inf" > "inf_primdef"
     7 
     8 const_maps
     9   "inf" > "HOL4Prob.prob_extra.inf"
    10   "COMPL" > "HOL4Base.pred_set.COMPL"
    11 
    12 thm_maps
    13   "inf_primdef" > "HOL4Prob.prob_extra.inf_primdef"
    14   "inf_def" > "HOL4Prob.prob_extra.inf_def"
    15   "X_HALF_HALF" > "HOL4Prob.prob_extra.X_HALF_HALF"
    16   "UNION_DISJOINT_SPLIT" > "HOL4Prob.prob_extra.UNION_DISJOINT_SPLIT"
    17   "UNION_DEF_ALT" > "HOL4Prob.prob_extra.UNION_DEF_ALT"
    18   "SUBSET_EQ_DECOMP" > "HOL4Base.pred_set.SUBSET_ANTISYM"
    19   "SUBSET_EQ" > "HOL4Prob.prob_extra.SUBSET_EQ"
    20   "SET_EQ_EXT" > "HOL4Base.pred_set.EXTENSION"
    21   "REAL_X_LE_SUP" > "HOL4Prob.prob_extra.REAL_X_LE_SUP"
    22   "REAL_SUP_MAX" > "HOL4Prob.prob_extra.REAL_SUP_MAX"
    23   "REAL_SUP_LE_X" > "HOL4Prob.prob_extra.REAL_SUP_LE_X"
    24   "REAL_SUP_EXISTS_UNIQUE" > "HOL4Prob.prob_extra.REAL_SUP_EXISTS_UNIQUE"
    25   "REAL_POW" > "RealPow.realpow_real_of_nat"
    26   "REAL_LE_INV_LE" > "Ring_and_Field.le_imp_inverse_le"
    27   "REAL_LE_EQ" > "Set.basic_trans_rules_26"
    28   "REAL_INVINV_ALL" > "Ring_and_Field.inverse_inverse_eq"
    29   "REAL_INF_MIN" > "HOL4Prob.prob_extra.REAL_INF_MIN"
    30   "RAND_THM" > "HOL.arg_cong"
    31   "POW_HALF_TWICE" > "HOL4Prob.prob_extra.POW_HALF_TWICE"
    32   "POW_HALF_POS" > "HOL4Prob.prob_extra.POW_HALF_POS"
    33   "POW_HALF_MONO" > "HOL4Prob.prob_extra.POW_HALF_MONO"
    34   "POW_HALF_EXP" > "HOL4Prob.prob_extra.POW_HALF_EXP"
    35   "ONE_MINUS_HALF" > "HOL4Prob.prob_extra.ONE_MINUS_HALF"
    36   "MOD_TWO" > "HOL4Prob.prob_extra.MOD_TWO"
    37   "MEM_NIL_MAP_CONS" > "HOL4Prob.prob_extra.MEM_NIL_MAP_CONS"
    38   "MEM_NIL" > "HOL4Prob.prob_extra.MEM_NIL"
    39   "MEM_FILTER" > "HOL4Prob.prob_extra.MEM_FILTER"
    40   "MAP_MEM" > "HOL4Prob.prob_extra.MAP_MEM"
    41   "MAP_ID" > "List.map_ident"
    42   "LENGTH_FILTER" > "List.length_filter_le"
    43   "LAST_MEM" > "HOL4Prob.prob_extra.LAST_MEM"
    44   "LAST_MAP_CONS" > "HOL4Prob.prob_extra.LAST_MAP_CONS"
    45   "IS_PREFIX_TRANS" > "HOL4Prob.prob_extra.IS_PREFIX_TRANS"
    46   "IS_PREFIX_SNOC" > "HOL4Prob.prob_extra.IS_PREFIX_SNOC"
    47   "IS_PREFIX_REFL" > "HOL4Prob.prob_extra.IS_PREFIX_REFL"
    48   "IS_PREFIX_NIL" > "HOL4Prob.prob_extra.IS_PREFIX_NIL"
    49   "IS_PREFIX_LENGTH_ANTI" > "HOL4Prob.prob_extra.IS_PREFIX_LENGTH_ANTI"
    50   "IS_PREFIX_LENGTH" > "HOL4Prob.prob_extra.IS_PREFIX_LENGTH"
    51   "IS_PREFIX_BUTLAST" > "HOL4Prob.prob_extra.IS_PREFIX_BUTLAST"
    52   "IS_PREFIX_ANTISYM" > "HOL4Prob.prob_extra.IS_PREFIX_ANTISYM"
    53   "IN_EMPTY" > "HOL4Base.pred_set.NOT_IN_EMPTY"
    54   "IN_COMPL" > "HOL4Base.pred_set.IN_COMPL"
    55   "INV_SUC_POS" > "HOL4Prob.prob_extra.INV_SUC_POS"
    56   "INV_SUC_MAX" > "HOL4Prob.prob_extra.INV_SUC_MAX"
    57   "INV_SUC" > "HOL4Prob.prob_extra.INV_SUC"
    58   "INTER_UNION_RDISTRIB" > "HOL4Prob.prob_extra.INTER_UNION_RDISTRIB"
    59   "INTER_UNION_COMPL" > "HOL4Base.pred_set.INTER_UNION_COMPL"
    60   "INTER_IS_EMPTY" > "HOL4Prob.prob_extra.INTER_IS_EMPTY"
    61   "INF_DEF_ALT" > "HOL4Prob.prob_extra.INF_DEF_ALT"
    62   "HALF_POS" > "HOL4Prob.prob_extra.HALF_POS"
    63   "HALF_LT_1" > "HOL4Prob.prob_extra.HALF_LT_1"
    64   "HALF_CANCEL" > "HOL4Prob.prob_extra.HALF_CANCEL"
    65   "GSPEC_DEF_ALT" > "HOL4Prob.prob_extra.GSPEC_DEF_ALT"
    66   "FOLDR_MAP" > "HOL4Prob.prob_extra.FOLDR_MAP"
    67   "FILTER_TRUE" > "HOL4Prob.prob_extra.FILTER_TRUE"
    68   "FILTER_OUT_ELT" > "HOL4Prob.prob_extra.FILTER_OUT_ELT"
    69   "FILTER_MEM" > "HOL4Prob.prob_extra.FILTER_MEM"
    70   "FILTER_FALSE" > "HOL4Prob.prob_extra.FILTER_FALSE"
    71   "EXP_DIV_TWO" > "HOL4Prob.prob_extra.EXP_DIV_TWO"
    72   "EXISTS_LONGEST" > "HOL4Prob.prob_extra.EXISTS_LONGEST"
    73   "EVEN_ODD_EXISTS_EQ" > "HOL4Prob.prob_extra.EVEN_ODD_EXISTS_EQ"
    74   "EVEN_ODD_BASIC" > "HOL4Prob.prob_extra.EVEN_ODD_BASIC"
    75   "EVEN_EXP_TWO" > "HOL4Prob.prob_extra.EVEN_EXP_TWO"
    76   "EQ_EXT_EQ" > "Fun.expand_fun_eq"
    77   "DIV_TWO_UNIQUE" > "HOL4Prob.prob_extra.DIV_TWO_UNIQUE"
    78   "DIV_TWO_MONO_EVEN" > "HOL4Prob.prob_extra.DIV_TWO_MONO_EVEN"
    79   "DIV_TWO_MONO" > "HOL4Prob.prob_extra.DIV_TWO_MONO"
    80   "DIV_TWO_EXP" > "HOL4Prob.prob_extra.DIV_TWO_EXP"
    81   "DIV_TWO_CANCEL" > "HOL4Prob.prob_extra.DIV_TWO_CANCEL"
    82   "DIV_TWO_BASIC" > "HOL4Prob.prob_extra.DIV_TWO_BASIC"
    83   "DIV_TWO" > "HOL4Prob.prob_extra.DIV_TWO"
    84   "DIV_THEN_MULT" > "HOL4Prob.prob_extra.DIV_THEN_MULT"
    85   "DIVISION_TWO" > "HOL4Prob.prob_extra.DIVISION_TWO"
    86   "COMPL_def" > "HOL4Base.pred_set.COMPL_DEF"
    87   "COMPL_SPLITS" > "HOL4Base.pred_set.COMPL_SPLITS"
    88   "COMPL_COMPL" > "HOL4Base.pred_set.COMPL_COMPL"
    89   "COMPL_CLAUSES" > "HOL4Base.pred_set.COMPL_CLAUSES"
    90   "BOOL_BOOL_CASES_THM" > "HOL4Prob.prob_extra.BOOL_BOOL_CASES_THM"
    91   "BOOL_BOOL_CASES" > "HOL4Base.bool.BOOL_FUN_INDUCT"
    92   "APPEND_MEM" > "HOL4Base.list.MEM_APPEND"
    93   "ABS_UNIT_INTERVAL" > "HOL4Prob.prob_extra.ABS_UNIT_INTERVAL"
    94   "ABS_BETWEEN_LE" > "HOL4Prob.prob_extra.ABS_BETWEEN_LE"
    95 
    96 end