src/HOL/Import/HOL/realax.imp
author haftmann
Thu, 17 May 2007 19:49:40 +0200
changeset 22997 d4f3b015b50b
parent 19277 f7602e74d948
child 23881 851c74f1bb69
permissions -rw-r--r--
canonical prefixing of class constants

import

import_segment "hol4"

def_maps
  "treal_of_hreal" > "treal_of_hreal_def"
  "treal_neg" > "treal_neg_def"
  "treal_mul" > "treal_mul_def"
  "treal_lt" > "treal_lt_def"
  "treal_inv" > "treal_inv_def"
  "treal_eq" > "treal_eq_def"
  "treal_add" > "treal_add_def"
  "treal_1" > "treal_1_def"
  "treal_0" > "treal_0_def"
  "hreal_of_treal" > "hreal_of_treal_def"

type_maps
  "real" > "RealDef.real"

const_maps
  "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal"
  "treal_neg" > "HOL4Real.realax.treal_neg"
  "treal_mul" > "HOL4Real.realax.treal_mul"
  "treal_lt" > "HOL4Real.realax.treal_lt"
  "treal_inv" > "HOL4Real.realax.treal_inv"
  "treal_eq" > "HOL4Real.realax.treal_eq"
  "treal_add" > "HOL4Real.realax.treal_add"
  "treal_1" > "HOL4Real.realax.treal_1"
  "treal_0" > "HOL4Real.realax.treal_0"
  "real_neg" > "HOL.minus_class.uminus" :: "real => real"
  "real_mul" > "HOL.times_class.times" :: "real => real => real"
  "real_lt" > "Orderings.ord_class.less" :: "real => real => bool"
  "real_add" > "HOL.plus_class.plus" :: "real => real => real"
  "real_1" > "HOL.one_class.one" :: "real"
  "real_0" > "HOL.zero_class.zero" :: "real"
  "inv" > "HOL.divide_class.inverse" :: "real => real"
  "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"

thm_maps
  "treal_of_hreal_def" > "HOL4Real.realax.treal_of_hreal_def"
  "treal_of_hreal" > "HOL4Real.realax.treal_of_hreal"
  "treal_neg_def" > "HOL4Real.realax.treal_neg_def"
  "treal_neg" > "HOL4Real.realax.treal_neg"
  "treal_mul_def" > "HOL4Real.realax.treal_mul_def"
  "treal_mul" > "HOL4Real.realax.treal_mul"
  "treal_lt_def" > "HOL4Real.realax.treal_lt_def"
  "treal_lt" > "HOL4Real.realax.treal_lt"
  "treal_inv_def" > "HOL4Real.realax.treal_inv_def"
  "treal_inv" > "HOL4Real.realax.treal_inv"
  "treal_eq_def" > "HOL4Real.realax.treal_eq_def"
  "treal_eq" > "HOL4Real.realax.treal_eq"
  "treal_add_def" > "HOL4Real.realax.treal_add_def"
  "treal_add" > "HOL4Real.realax.treal_add"
  "treal_1_def" > "HOL4Real.realax.treal_1_def"
  "treal_1" > "HOL4Real.realax.treal_1"
  "treal_0_def" > "HOL4Real.realax.treal_0_def"
  "treal_0" > "HOL4Real.realax.treal_0"
  "hreal_of_treal_def" > "HOL4Real.realax.hreal_of_treal_def"
  "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
  "TREAL_NEG_WELLDEF" > "HOL4Real.realax.TREAL_NEG_WELLDEF"
  "TREAL_MUL_WELLDEFR" > "HOL4Real.realax.TREAL_MUL_WELLDEFR"
  "TREAL_MUL_WELLDEF" > "HOL4Real.realax.TREAL_MUL_WELLDEF"
  "TREAL_MUL_SYM" > "HOL4Real.realax.TREAL_MUL_SYM"
  "TREAL_MUL_LINV" > "HOL4Real.realax.TREAL_MUL_LINV"
  "TREAL_MUL_LID" > "HOL4Real.realax.TREAL_MUL_LID"
  "TREAL_MUL_ASSOC" > "HOL4Real.realax.TREAL_MUL_ASSOC"
  "TREAL_LT_WELLDEFR" > "HOL4Real.realax.TREAL_LT_WELLDEFR"
  "TREAL_LT_WELLDEFL" > "HOL4Real.realax.TREAL_LT_WELLDEFL"
  "TREAL_LT_WELLDEF" > "HOL4Real.realax.TREAL_LT_WELLDEF"
  "TREAL_LT_TRANS" > "HOL4Real.realax.TREAL_LT_TRANS"
  "TREAL_LT_TOTAL" > "HOL4Real.realax.TREAL_LT_TOTAL"
  "TREAL_LT_REFL" > "HOL4Real.realax.TREAL_LT_REFL"
  "TREAL_LT_MUL" > "HOL4Real.realax.TREAL_LT_MUL"
  "TREAL_LT_ADD" > "HOL4Real.realax.TREAL_LT_ADD"
  "TREAL_LDISTRIB" > "HOL4Real.realax.TREAL_LDISTRIB"
  "TREAL_ISO" > "HOL4Real.realax.TREAL_ISO"
  "TREAL_INV_WELLDEF" > "HOL4Real.realax.TREAL_INV_WELLDEF"
  "TREAL_INV_0" > "HOL4Real.realax.TREAL_INV_0"
  "TREAL_EQ_TRANS" > "HOL4Real.realax.TREAL_EQ_TRANS"
  "TREAL_EQ_SYM" > "HOL4Real.realax.TREAL_EQ_SYM"
  "TREAL_EQ_REFL" > "HOL4Real.realax.TREAL_EQ_REFL"
  "TREAL_EQ_EQUIV" > "HOL4Real.realax.TREAL_EQ_EQUIV"
  "TREAL_EQ_AP" > "HOL4Real.realax.TREAL_EQ_AP"
  "TREAL_BIJ_WELLDEF" > "HOL4Real.realax.TREAL_BIJ_WELLDEF"
  "TREAL_BIJ" > "HOL4Real.realax.TREAL_BIJ"
  "TREAL_ADD_WELLDEFR" > "HOL4Real.realax.TREAL_ADD_WELLDEFR"
  "TREAL_ADD_WELLDEF" > "HOL4Real.realax.TREAL_ADD_WELLDEF"
  "TREAL_ADD_SYM" > "HOL4Real.realax.TREAL_ADD_SYM"
  "TREAL_ADD_LINV" > "HOL4Real.realax.TREAL_ADD_LINV"
  "TREAL_ADD_LID" > "HOL4Real.realax.TREAL_ADD_LID"
  "TREAL_ADD_ASSOC" > "HOL4Real.realax.TREAL_ADD_ASSOC"
  "TREAL_10" > "HOL4Real.realax.TREAL_10"
  "REAL_SUP_ALLPOS" > "HOL4Compat.REAL_SUP_ALLPOS"
  "REAL_MUL_SYM" > "IntDef.zmult_ac_2"
  "REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
  "REAL_MUL_LID" > "Finite_Set.AC_mult.f_e.left_ident"
  "REAL_MUL_ASSOC" > "HOL4Compat.REAL_MUL_ASSOC"
  "REAL_LT_TRANS" > "Set.basic_trans_rules_21"
  "REAL_LT_TOTAL" > "HOL4Compat.REAL_LT_TOTAL"
  "REAL_LT_REFL" > "Orderings.order_less_irrefl"
  "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos"
  "REAL_LT_IADD" > "OrderedGroup.add_strict_left_mono"
  "REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_2"
  "REAL_INV_0" > "Ring_and_Field.division_by_zero_class.inverse_zero"
  "REAL_ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
  "REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
  "REAL_ADD_LID" > "Finite_Set.AC_add.f_e.left_ident"
  "REAL_ADD_ASSOC" > "HOL4Compat.REAL_ADD_ASSOC"
  "REAL_10" > "HOL4Compat.REAL_10"
  "HREAL_RDISTRIB" > "HOL4Real.realax.HREAL_RDISTRIB"
  "HREAL_LT_REFL" > "HOL4Real.realax.HREAL_LT_REFL"
  "HREAL_LT_NE" > "HOL4Real.realax.HREAL_LT_NE"
  "HREAL_LT_LADD" > "HOL4Real.realax.HREAL_LT_LADD"
  "HREAL_LT_GT" > "HOL4Real.realax.HREAL_LT_GT"
  "HREAL_LT_ADDR" > "HOL4Real.realax.HREAL_LT_ADDR"
  "HREAL_LT_ADDL" > "HOL4Real.realax.HREAL_LT_ADDL"
  "HREAL_LT_ADD2" > "HOL4Real.realax.HREAL_LT_ADD2"
  "HREAL_EQ_LADD" > "HOL4Real.realax.HREAL_EQ_LADD"
  "HREAL_EQ_ADDR" > "HOL4Base.hreal.HREAL_NOZERO"
  "HREAL_EQ_ADDL" > "HOL4Real.realax.HREAL_EQ_ADDL"

ignore_thms
  "real_tybij"
  "real_of_hreal"
  "real_neg"
  "real_mul"
  "real_lt"
  "real_inv"
  "real_add"
  "real_TY_DEF"
  "real_1"
  "real_0"
  "hreal_of_real"
  "SUP_ALLPOS_LEMMA4"
  "SUP_ALLPOS_LEMMA3"
  "SUP_ALLPOS_LEMMA2"
  "SUP_ALLPOS_LEMMA1"
  "REAL_POS"
  "REAL_ISO_EQ"

end