src/HOL/Import/HOL/hreal.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   "isacut" > "isacut_def"
     7   "hreal_sup" > "hreal_sup_def"
     8   "hreal_sub" > "hreal_sub_def"
     9   "hreal_mul" > "hreal_mul_def"
    10   "hreal_lt" > "hreal_lt_def"
    11   "hreal_inv" > "hreal_inv_def"
    12   "hreal_add" > "hreal_add_def"
    13   "hreal_1" > "hreal_1_def"
    14   "hreal" > "hreal_def"
    15   "hrat_lt" > "hrat_lt_def"
    16   "cut_of_hrat" > "cut_of_hrat_def"
    17   "cut" > "cut_def"
    18 
    19 type_maps
    20   "hreal" > "HOL4Base.hreal.hreal"
    21 
    22 const_maps
    23   "isacut" > "HOL4Base.hreal.isacut"
    24   "hreal_sup" > "HOL4Base.hreal.hreal_sup"
    25   "hreal_sub" > "HOL4Base.hreal.hreal_sub"
    26   "hreal_mul" > "HOL4Base.hreal.hreal_mul"
    27   "hreal_lt" > "HOL4Base.hreal.hreal_lt"
    28   "hreal_inv" > "HOL4Base.hreal.hreal_inv"
    29   "hreal_add" > "HOL4Base.hreal.hreal_add"
    30   "hreal_1" > "HOL4Base.hreal.hreal_1"
    31   "hrat_lt" > "HOL4Base.hreal.hrat_lt"
    32   "cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
    33 
    34 thm_maps
    35   "isacut_def" > "HOL4Base.hreal.isacut_def"
    36   "isacut" > "HOL4Base.hreal.isacut"
    37   "hreal_tybij" > "HOL4Base.hreal.hreal_tybij"
    38   "hreal_sup_def" > "HOL4Base.hreal.hreal_sup_def"
    39   "hreal_sup" > "HOL4Base.hreal.hreal_sup"
    40   "hreal_sub_def" > "HOL4Base.hreal.hreal_sub_def"
    41   "hreal_sub" > "HOL4Base.hreal.hreal_sub"
    42   "hreal_mul_def" > "HOL4Base.hreal.hreal_mul_def"
    43   "hreal_mul" > "HOL4Base.hreal.hreal_mul"
    44   "hreal_lt_def" > "HOL4Base.hreal.hreal_lt_def"
    45   "hreal_lt" > "HOL4Base.hreal.hreal_lt"
    46   "hreal_inv_def" > "HOL4Base.hreal.hreal_inv_def"
    47   "hreal_inv" > "HOL4Base.hreal.hreal_inv"
    48   "hreal_add_def" > "HOL4Base.hreal.hreal_add_def"
    49   "hreal_add" > "HOL4Base.hreal.hreal_add"
    50   "hreal_TY_DEF" > "HOL4Base.hreal.hreal_TY_DEF"
    51   "hreal_1_def" > "HOL4Base.hreal.hreal_1_def"
    52   "hreal_1" > "HOL4Base.hreal.hreal_1"
    53   "hrat_lt_def" > "HOL4Base.hreal.hrat_lt_def"
    54   "hrat_lt" > "HOL4Base.hreal.hrat_lt"
    55   "cut_of_hrat_def" > "HOL4Base.hreal.cut_of_hrat_def"
    56   "cut_of_hrat" > "HOL4Base.hreal.cut_of_hrat"
    57   "ISACUT_HRAT" > "HOL4Base.hreal.ISACUT_HRAT"
    58   "HREAL_SUP_ISACUT" > "HOL4Base.hreal.HREAL_SUP_ISACUT"
    59   "HREAL_SUP" > "HOL4Base.hreal.HREAL_SUP"
    60   "HREAL_SUB_ISACUT" > "HOL4Base.hreal.HREAL_SUB_ISACUT"
    61   "HREAL_SUB_ADD" > "HOL4Base.hreal.HREAL_SUB_ADD"
    62   "HREAL_NOZERO" > "HOL4Base.hreal.HREAL_NOZERO"
    63   "HREAL_MUL_SYM" > "HOL4Base.hreal.HREAL_MUL_SYM"
    64   "HREAL_MUL_LINV" > "HOL4Base.hreal.HREAL_MUL_LINV"
    65   "HREAL_MUL_LID" > "HOL4Base.hreal.HREAL_MUL_LID"
    66   "HREAL_MUL_ISACUT" > "HOL4Base.hreal.HREAL_MUL_ISACUT"
    67   "HREAL_MUL_ASSOC" > "HOL4Base.hreal.HREAL_MUL_ASSOC"
    68   "HREAL_LT_TOTAL" > "HOL4Base.hreal.HREAL_LT_TOTAL"
    69   "HREAL_LT_LEMMA" > "HOL4Base.hreal.HREAL_LT_LEMMA"
    70   "HREAL_LT" > "HOL4Base.hreal.HREAL_LT"
    71   "HREAL_LDISTRIB" > "HOL4Base.hreal.HREAL_LDISTRIB"
    72   "HREAL_INV_ISACUT" > "HOL4Base.hreal.HREAL_INV_ISACUT"
    73   "HREAL_ADD_TOTAL" > "HOL4Base.hreal.HREAL_ADD_TOTAL"
    74   "HREAL_ADD_SYM" > "HOL4Base.hreal.HREAL_ADD_SYM"
    75   "HREAL_ADD_ISACUT" > "HOL4Base.hreal.HREAL_ADD_ISACUT"
    76   "HREAL_ADD_ASSOC" > "HOL4Base.hreal.HREAL_ADD_ASSOC"
    77   "HRAT_UP" > "HOL4Base.hreal.HRAT_UP"
    78   "HRAT_RDISTRIB" > "HOL4Base.hreal.HRAT_RDISTRIB"
    79   "HRAT_MUL_RINV" > "HOL4Base.hreal.HRAT_MUL_RINV"
    80   "HRAT_MUL_RID" > "HOL4Base.hreal.HRAT_MUL_RID"
    81   "HRAT_MEAN" > "HOL4Base.hreal.HRAT_MEAN"
    82   "HRAT_LT_TRANS" > "HOL4Base.hreal.HRAT_LT_TRANS"
    83   "HRAT_LT_TOTAL" > "HOL4Base.hreal.HRAT_LT_TOTAL"
    84   "HRAT_LT_RMUL1" > "HOL4Base.hreal.HRAT_LT_RMUL1"
    85   "HRAT_LT_RMUL" > "HOL4Base.hreal.HRAT_LT_RMUL"
    86   "HRAT_LT_REFL" > "HOL4Base.hreal.HRAT_LT_REFL"
    87   "HRAT_LT_RADD" > "HOL4Base.hreal.HRAT_LT_RADD"
    88   "HRAT_LT_R1" > "HOL4Base.hreal.HRAT_LT_R1"
    89   "HRAT_LT_NE" > "HOL4Base.hreal.HRAT_LT_NE"
    90   "HRAT_LT_MUL2" > "HOL4Base.hreal.HRAT_LT_MUL2"
    91   "HRAT_LT_LMUL1" > "HOL4Base.hreal.HRAT_LT_LMUL1"
    92   "HRAT_LT_LMUL" > "HOL4Base.hreal.HRAT_LT_LMUL"
    93   "HRAT_LT_LADD" > "HOL4Base.hreal.HRAT_LT_LADD"
    94   "HRAT_LT_L1" > "HOL4Base.hreal.HRAT_LT_L1"
    95   "HRAT_LT_GT" > "HOL4Base.hreal.HRAT_LT_GT"
    96   "HRAT_LT_ANTISYM" > "HOL4Base.hreal.HRAT_LT_ANTISYM"
    97   "HRAT_LT_ADDR" > "HOL4Base.hreal.HRAT_LT_ADDR"
    98   "HRAT_LT_ADDL" > "HOL4Base.hreal.HRAT_LT_ADDL"
    99   "HRAT_LT_ADD2" > "HOL4Base.hreal.HRAT_LT_ADD2"
   100   "HRAT_INV_MUL" > "HOL4Base.hreal.HRAT_INV_MUL"
   101   "HRAT_GT_LMUL1" > "HOL4Base.hreal.HRAT_GT_LMUL1"
   102   "HRAT_GT_L1" > "HOL4Base.hreal.HRAT_GT_L1"
   103   "HRAT_EQ_LMUL" > "HOL4Base.hreal.HRAT_EQ_LMUL"
   104   "HRAT_EQ_LADD" > "HOL4Base.hreal.HRAT_EQ_LADD"
   105   "HRAT_DOWN2" > "HOL4Base.hreal.HRAT_DOWN2"
   106   "HRAT_DOWN" > "HOL4Base.hreal.HRAT_DOWN"
   107   "EQUAL_CUTS" > "HOL4Base.hreal.EQUAL_CUTS"
   108   "CUT_UP" > "HOL4Base.hreal.CUT_UP"
   109   "CUT_UBOUND" > "HOL4Base.hreal.CUT_UBOUND"
   110   "CUT_STRADDLE" > "HOL4Base.hreal.CUT_STRADDLE"
   111   "CUT_NONEMPTY" > "HOL4Base.hreal.CUT_NONEMPTY"
   112   "CUT_NEARTOP_MUL" > "HOL4Base.hreal.CUT_NEARTOP_MUL"
   113   "CUT_NEARTOP_ADD" > "HOL4Base.hreal.CUT_NEARTOP_ADD"
   114   "CUT_ISACUT" > "HOL4Base.hreal.CUT_ISACUT"
   115   "CUT_DOWN" > "HOL4Base.hreal.CUT_DOWN"
   116   "CUT_BOUNDED" > "HOL4Base.hreal.CUT_BOUNDED"
   117 
   118 end