Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL/realax.imp
changeset 14516 a183dec876ab
child 14620 1be590fd2422 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL/realax.imp	Fri Apr 02 17:37:45 2004 +0200
@@ -0,0 +1,141 @@
+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.mult_ac_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_distrib_1"
+  "REAL_INV_0" > "Ring_and_Field.division_by_zero.inverse_zero"
+  "REAL_ADD_SYM" > "Ring_and_Field.add_ac_2"
+  "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
isabelle