Minor cleanup of headers and some speedup of the HOL4 import.
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" > "uminus" :: "real => real"
"real_mul" > "op *" :: "real => real => real"
"real_lt" > "op <" :: "real => real => bool"
"real_add" > "op +" :: "real => real => real"
"real_1" > "1" :: "real"
"real_0" > "0" :: "real"
"inv" > "HOL.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" > "Ring_and_Field.ring_eq_simps_2"
"REAL_MUL_LINV" > "HOL4Compat.REAL_MUL_LINV"
"REAL_MUL_LID" > "Ring_and_Field.almost_semiring.mult_1"
"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" > "HOL.order_less_irrefl"
"REAL_LT_MUL" > "Ring_and_Field.mult_pos"
"REAL_LT_IADD" > "Ring_and_Field.add_strict_left_mono"
"REAL_LDISTRIB" > "Ring_and_Field.ring_eq_simps_5"
"REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
"REAL_ADD_SYM" > "Ring_and_Field.ring_eq_simps_9"
"REAL_ADD_LINV" > "HOL4Compat.REAL_ADD_LINV"
"REAL_ADD_LID" > "Ring_and_Field.abelian_semigroup.add_0"
"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