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 22997 d4f3b015b50b
parent 19277 f7602e74d948
child 23881 851c74f1bb69 
--- a/src/HOL/Import/HOL/real.imp	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Import/HOL/real.imp	Thu May 17 19:49:40 2007 +0200
@@ -10,14 +10,14 @@
 const_maps
   "sup" > "HOL4Real.real.sup"
   "sum" > "HOL4Real.real.sum"
-  "real_sub" > "HOL.minus" :: "real => real => real"
+  "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
   "real_of_num" > "RealDef.real" :: "nat => real"
-  "real_lte" > "Orderings.less_eq" :: "real => real => bool"
+  "real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool"
   "real_gt" > "HOL4Compat.real_gt"
   "real_ge" > "HOL4Compat.real_ge"
-  "pow" > "Nat.power" :: "real => nat => real"
-  "abs" > "HOL.abs" :: "real => real"
-  "/" > "HOL.divide" :: "real => real => real"
+  "pow" > "Nat.power_class.power" :: "real => nat => real"
+  "abs" > "HOL.minus_class.abs" :: "real => real"
+  "/" > "HOL.divides_class.divide" :: "real => real => real"
 
 thm_maps
   "sup_def" > "HOL4Real.real.sup_def"
isabelle