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/real.imp
changeset 16775 c1b87ef4a1c3
parent 15647 b1f486a9c56b
child 17188 a26a4fc323ed 
--- a/src/HOL/Import/HOL/real.imp	Tue Jul 12 12:49:46 2005 +0200
+++ b/src/HOL/Import/HOL/real.imp	Tue Jul 12 17:56:03 2005 +0200
@@ -160,7 +160,7 @@
   "REAL_LT_NEG" > "OrderedGroup.neg_less_iff_less"
   "REAL_LT_MULTIPLE" > "HOL4Real.real.REAL_LT_MULTIPLE"
   "REAL_LT_MUL2" > "Ring_and_Field.mult_strict_mono'"
-  "REAL_LT_MUL" > "Ring_and_Field.mult_pos"
+  "REAL_LT_MUL" > "Ring_and_Field.mult_pos_pos"
   "REAL_LT_LMUL_IMP" > "Ring_and_Field.ordered_comm_semiring_strict.mult_strict_mono"
   "REAL_LT_LMUL_0" > "HOL4Real.real.REAL_LT_LMUL_0"
   "REAL_LT_LMUL" > "HOL4Real.real.REAL_LT_LMUL"
@@ -217,7 +217,7 @@
   "REAL_LE_NEG2" > "OrderedGroup.neg_le_iff_le"
   "REAL_LE_NEG" > "OrderedGroup.neg_le_iff_le"
   "REAL_LE_MUL2" > "HOL4Real.real.REAL_LE_MUL2"
-  "REAL_LE_MUL" > "Ring_and_Field.mult_pos_le"
+  "REAL_LE_MUL" > "Ring_and_Field.mult_nonneg_nonneg"
   "REAL_LE_LT" > "Orderings.order_le_less"
   "REAL_LE_LNEG" > "RealDef.real_0_le_add_iff"
   "REAL_LE_LMUL_IMP" > "Ring_and_Field.pordered_comm_semiring.mult_mono"
isabelle