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