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 19277 f7602e74d948
parent 19233 77ca20b0ed77
child 22997 d4f3b015b50b 
--- a/src/HOL/Import/HOL/realax.imp	Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Import/HOL/realax.imp	Fri Mar 17 09:34:23 2006 +0100
@@ -29,7 +29,7 @@
   "treal_0" > "HOL4Real.realax.treal_0"
   "real_neg" > "HOL.uminus" :: "real => real"
   "real_mul" > "HOL.times" :: "real => real => real"
-  "real_lt" > "op <" :: "real => real => bool"
+  "real_lt" > "Orderings.less" :: "real => real => bool"
   "real_add" > "HOL.plus" :: "real => real => real"
   "real_1" > "1" :: "real"
   "real_0" > "0" :: "real"
isabelle