src/HOL/Import/HOL/poly.imp
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 14516 a183dec876ab
child 37887 2ae085b07f2f
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
  "rsquarefree" > "rsquarefree_def"
skalberg@14516
     7
  "poly_order" > "poly_order_def"
skalberg@14516
     8
  "poly_neg" > "poly_neg_primdef"
skalberg@14516
     9
  "poly_mul" > "poly_mul_primdef"
skalberg@14516
    10
  "poly_exp" > "poly_exp_primdef"
skalberg@14516
    11
  "poly_divides" > "poly_divides_def"
skalberg@14516
    12
  "poly_diff_aux" > "poly_diff_aux_primdef"
skalberg@14516
    13
  "poly_add" > "poly_add_primdef"
skalberg@14516
    14
  "poly" > "poly_primdef"
skalberg@14516
    15
  "normalize" > "normalize_def"
skalberg@14516
    16
  "diff" > "diff_def"
skalberg@14516
    17
  "degree" > "degree_def"
skalberg@14516
    18
  "##" > "##_def"
skalberg@14516
    19
skalberg@14516
    20
const_maps
skalberg@14516
    21
  "rsquarefree" > "HOL4Real.poly.rsquarefree"
skalberg@14516
    22
  "poly_order" > "HOL4Real.poly.poly_order"
skalberg@14516
    23
  "poly_neg" > "HOL4Real.poly.poly_neg"
skalberg@14516
    24
  "poly_divides" > "HOL4Real.poly.poly_divides"
skalberg@14516
    25
  "diff" > "HOL4Real.poly.diff"
skalberg@14516
    26
  "degree" > "HOL4Real.poly.degree"
skalberg@14516
    27
skalberg@14516
    28
thm_maps
skalberg@14516
    29
  "rsquarefree_def" > "HOL4Real.poly.rsquarefree_def"
skalberg@14516
    30
  "rsquarefree" > "HOL4Real.poly.rsquarefree"
skalberg@14516
    31
  "poly_order_def" > "HOL4Real.poly.poly_order_def"
skalberg@14516
    32
  "poly_order" > "HOL4Real.poly.poly_order"
skalberg@14516
    33
  "poly_neg_primdef" > "HOL4Real.poly.poly_neg_primdef"
skalberg@14516
    34
  "poly_neg_def" > "HOL4Real.poly.poly_neg_def"
skalberg@14516
    35
  "poly_mul_def" > "HOL4Real.poly.poly_mul_def"
skalberg@14516
    36
  "poly_exp_def" > "HOL4Real.poly.poly_exp_def"
skalberg@14516
    37
  "poly_divides_def" > "HOL4Real.poly.poly_divides_def"
skalberg@14516
    38
  "poly_divides" > "HOL4Real.poly.poly_divides"
skalberg@14516
    39
  "poly_diff_def" > "HOL4Real.poly.poly_diff_def"
skalberg@14516
    40
  "poly_diff_aux_def" > "HOL4Real.poly.poly_diff_aux_def"
skalberg@14516
    41
  "poly_def" > "HOL4Real.poly.poly_def"
skalberg@14516
    42
  "poly_cmul_def" > "HOL4Real.poly.poly_cmul_def"
skalberg@14516
    43
  "poly_add_def" > "HOL4Real.poly.poly_add_def"
skalberg@14516
    44
  "normalize" > "HOL4Real.poly.normalize"
skalberg@14516
    45
  "diff_def" > "HOL4Real.poly.diff_def"
skalberg@14516
    46
  "degree_def" > "HOL4Real.poly.degree_def"
skalberg@14516
    47
  "degree" > "HOL4Real.poly.degree"
skalberg@14516
    48
  "RSQUAREFREE_ROOTS" > "HOL4Real.poly.RSQUAREFREE_ROOTS"
skalberg@14516
    49
  "RSQUAREFREE_DECOMP" > "HOL4Real.poly.RSQUAREFREE_DECOMP"
skalberg@14516
    50
  "POLY_ZERO_LEMMA" > "HOL4Real.poly.POLY_ZERO_LEMMA"
skalberg@14516
    51
  "POLY_ZERO" > "HOL4Real.poly.POLY_ZERO"
skalberg@14516
    52
  "POLY_SQUAREFREE_DECOMP_ORDER" > "HOL4Real.poly.POLY_SQUAREFREE_DECOMP_ORDER"
skalberg@14516
    53
  "POLY_SQUAREFREE_DECOMP" > "HOL4Real.poly.POLY_SQUAREFREE_DECOMP"
skalberg@14516
    54
  "POLY_ROOTS_INDEX_LENGTH" > "HOL4Real.poly.POLY_ROOTS_INDEX_LENGTH"
skalberg@14516
    55
  "POLY_ROOTS_INDEX_LEMMA" > "HOL4Real.poly.POLY_ROOTS_INDEX_LEMMA"
skalberg@14516
    56
  "POLY_ROOTS_FINITE_SET" > "HOL4Real.poly.POLY_ROOTS_FINITE_SET"
skalberg@14516
    57
  "POLY_ROOTS_FINITE_LEMMA" > "HOL4Real.poly.POLY_ROOTS_FINITE_LEMMA"
skalberg@14516
    58
  "POLY_ROOTS_FINITE" > "HOL4Real.poly.POLY_ROOTS_FINITE"
skalberg@14516
    59
  "POLY_PRIME_EQ_0" > "HOL4Real.poly.POLY_PRIME_EQ_0"
skalberg@14516
    60
  "POLY_PRIMES" > "HOL4Real.poly.POLY_PRIMES"
skalberg@14516
    61
  "POLY_ORDER_EXISTS" > "HOL4Real.poly.POLY_ORDER_EXISTS"
skalberg@14516
    62
  "POLY_ORDER" > "HOL4Real.poly.POLY_ORDER"
skalberg@14516
    63
  "POLY_NORMALIZE" > "HOL4Real.poly.POLY_NORMALIZE"
skalberg@14516
    64
  "POLY_NEG_CLAUSES" > "HOL4Real.poly.POLY_NEG_CLAUSES"
skalberg@14516
    65
  "POLY_NEG" > "HOL4Real.poly.POLY_NEG"
skalberg@14516
    66
  "POLY_MVT" > "HOL4Real.poly.POLY_MVT"
skalberg@14516
    67
  "POLY_MUL_LCANCEL" > "HOL4Real.poly.POLY_MUL_LCANCEL"
skalberg@14516
    68
  "POLY_MUL_CLAUSES" > "HOL4Real.poly.POLY_MUL_CLAUSES"
skalberg@14516
    69
  "POLY_MUL_ASSOC" > "HOL4Real.poly.POLY_MUL_ASSOC"
skalberg@14516
    70
  "POLY_MUL" > "HOL4Real.poly.POLY_MUL"
skalberg@14516
    71
  "POLY_MONO" > "HOL4Real.poly.POLY_MONO"
skalberg@14516
    72
  "POLY_LINEAR_REM" > "HOL4Real.poly.POLY_LINEAR_REM"
skalberg@14516
    73
  "POLY_LINEAR_DIVIDES" > "HOL4Real.poly.POLY_LINEAR_DIVIDES"
skalberg@14516
    74
  "POLY_LENGTH_MUL" > "HOL4Real.poly.POLY_LENGTH_MUL"
skalberg@14516
    75
  "POLY_IVT_POS" > "HOL4Real.poly.POLY_IVT_POS"
skalberg@14516
    76
  "POLY_IVT_NEG" > "HOL4Real.poly.POLY_IVT_NEG"
skalberg@14516
    77
  "POLY_EXP_PRIME_EQ_0" > "HOL4Real.poly.POLY_EXP_PRIME_EQ_0"
skalberg@14516
    78
  "POLY_EXP_EQ_0" > "HOL4Real.poly.POLY_EXP_EQ_0"
skalberg@14516
    79
  "POLY_EXP_DIVIDES" > "HOL4Real.poly.POLY_EXP_DIVIDES"
skalberg@14516
    80
  "POLY_EXP_ADD" > "HOL4Real.poly.POLY_EXP_ADD"
skalberg@14516
    81
  "POLY_EXP" > "HOL4Real.poly.POLY_EXP"
skalberg@14516
    82
  "POLY_ENTIRE_LEMMA" > "HOL4Real.poly.POLY_ENTIRE_LEMMA"
skalberg@14516
    83
  "POLY_ENTIRE" > "HOL4Real.poly.POLY_ENTIRE"
skalberg@14516
    84
  "POLY_DIVIDES_ZERO" > "HOL4Real.poly.POLY_DIVIDES_ZERO"
skalberg@14516
    85
  "POLY_DIVIDES_TRANS" > "HOL4Real.poly.POLY_DIVIDES_TRANS"
skalberg@14516
    86
  "POLY_DIVIDES_SUB2" > "HOL4Real.poly.POLY_DIVIDES_SUB2"
skalberg@14516
    87
  "POLY_DIVIDES_SUB" > "HOL4Real.poly.POLY_DIVIDES_SUB"
skalberg@14516
    88
  "POLY_DIVIDES_REFL" > "HOL4Real.poly.POLY_DIVIDES_REFL"
skalberg@14516
    89
  "POLY_DIVIDES_EXP" > "HOL4Real.poly.POLY_DIVIDES_EXP"
skalberg@14516
    90
  "POLY_DIVIDES_ADD" > "HOL4Real.poly.POLY_DIVIDES_ADD"
skalberg@14516
    91
  "POLY_DIFF_ZERO" > "HOL4Real.poly.POLY_DIFF_ZERO"
skalberg@14516
    92
  "POLY_DIFF_WELLDEF" > "HOL4Real.poly.POLY_DIFF_WELLDEF"
skalberg@14516
    93
  "POLY_DIFF_NEG" > "HOL4Real.poly.POLY_DIFF_NEG"
skalberg@14516
    94
  "POLY_DIFF_MUL_LEMMA" > "HOL4Real.poly.POLY_DIFF_MUL_LEMMA"
skalberg@14516
    95
  "POLY_DIFF_MUL" > "HOL4Real.poly.POLY_DIFF_MUL"
skalberg@14516
    96
  "POLY_DIFF_LEMMA" > "HOL4Real.poly.POLY_DIFF_LEMMA"
skalberg@14516
    97
  "POLY_DIFF_ISZERO" > "HOL4Real.poly.POLY_DIFF_ISZERO"
skalberg@14516
    98
  "POLY_DIFF_EXP_PRIME" > "HOL4Real.poly.POLY_DIFF_EXP_PRIME"
skalberg@14516
    99
  "POLY_DIFF_EXP" > "HOL4Real.poly.POLY_DIFF_EXP"
skalberg@14516
   100
  "POLY_DIFF_CMUL" > "HOL4Real.poly.POLY_DIFF_CMUL"
skalberg@14516
   101
  "POLY_DIFF_CLAUSES" > "HOL4Real.poly.POLY_DIFF_CLAUSES"
skalberg@14516
   102
  "POLY_DIFF_AUX_NEG" > "HOL4Real.poly.POLY_DIFF_AUX_NEG"
skalberg@14516
   103
  "POLY_DIFF_AUX_MUL_LEMMA" > "HOL4Real.poly.POLY_DIFF_AUX_MUL_LEMMA"
skalberg@14516
   104
  "POLY_DIFF_AUX_ISZERO" > "HOL4Real.poly.POLY_DIFF_AUX_ISZERO"
skalberg@14516
   105
  "POLY_DIFF_AUX_CMUL" > "HOL4Real.poly.POLY_DIFF_AUX_CMUL"
skalberg@14516
   106
  "POLY_DIFF_AUX_ADD" > "HOL4Real.poly.POLY_DIFF_AUX_ADD"
skalberg@14516
   107
  "POLY_DIFF_ADD" > "HOL4Real.poly.POLY_DIFF_ADD"
skalberg@14516
   108
  "POLY_DIFFERENTIABLE" > "HOL4Real.poly.POLY_DIFFERENTIABLE"
skalberg@14516
   109
  "POLY_DIFF" > "HOL4Real.poly.POLY_DIFF"
skalberg@14516
   110
  "POLY_CONT" > "HOL4Real.poly.POLY_CONT"
skalberg@14516
   111
  "POLY_CMUL_CLAUSES" > "HOL4Real.poly.POLY_CMUL_CLAUSES"
skalberg@14516
   112
  "POLY_CMUL" > "HOL4Real.poly.POLY_CMUL"
skalberg@14516
   113
  "POLY_ADD_RZERO" > "HOL4Real.poly.POLY_ADD_RZERO"
skalberg@14516
   114
  "POLY_ADD_CLAUSES" > "HOL4Real.poly.POLY_ADD_CLAUSES"
skalberg@14516
   115
  "POLY_ADD" > "HOL4Real.poly.POLY_ADD"
skalberg@14516
   116
  "ORDER_UNIQUE" > "HOL4Real.poly.ORDER_UNIQUE"
skalberg@14516
   117
  "ORDER_THM" > "HOL4Real.poly.ORDER_THM"
skalberg@14516
   118
  "ORDER_ROOT" > "HOL4Real.poly.ORDER_ROOT"
skalberg@14516
   119
  "ORDER_POLY" > "HOL4Real.poly.ORDER_POLY"
skalberg@14516
   120
  "ORDER_MUL" > "HOL4Real.poly.ORDER_MUL"
skalberg@14516
   121
  "ORDER_DIVIDES" > "HOL4Real.poly.ORDER_DIVIDES"
skalberg@14516
   122
  "ORDER_DIFF" > "HOL4Real.poly.ORDER_DIFF"
skalberg@14516
   123
  "ORDER_DECOMP" > "HOL4Real.poly.ORDER_DECOMP"
skalberg@14516
   124
  "ORDER" > "HOL4Real.poly.ORDER"
skalberg@14516
   125
  "FINITE_LEMMA" > "HOL4Real.poly.FINITE_LEMMA"
skalberg@14516
   126
  "DEGREE_ZERO" > "HOL4Real.poly.DEGREE_ZERO"
skalberg@14516
   127
skalberg@14516
   128
end