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