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 34974 18b41bba42b5
parent 25930 83e3dd60affe
child 35050 9f841f20dca6 
--- a/src/HOL/Import/HOL/realax.imp	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOL/realax.imp	Thu Jan 28 11:48:49 2010 +0100
@@ -27,13 +27,13 @@
   "treal_add" > "HOL4Real.realax.treal_add"
   "treal_1" > "HOL4Real.realax.treal_1"
   "treal_0" > "HOL4Real.realax.treal_0"
-  "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
-  "real_mul" > "HOL.times_class.times" :: "real => real => real"
-  "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
-  "real_add" > "HOL.plus_class.plus" :: "real => real => real"
-  "real_1" > "HOL.one_class.one" :: "real"
-  "real_0" > "HOL.zero_class.zero" :: "real"
-  "inv" > "HOL.divide_class.inverse" :: "real => real"
+  "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
+  "real_mul" > "Algebras.times_class.times" :: "real => real => real"
+  "real_lt" > "Algebras.ord_class.less" :: "real => real => bool"
+  "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
+  "real_1" > "Algebras.one_class.one" :: "real"
+  "real_0" > "Algebras.zero_class.zero" :: "real"
+  "inv" > "Algebras.divide_class.inverse" :: "real => real"
   "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
 
 thm_maps
isabelle