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/HOLLight/hollight.imp
changeset 34974 18b41bba42b5
parent 30925 c38cbc0ac8d1
child 35267 8dfd816713c6 
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Jan 28 11:48:49 2010 +0100
@@ -238,10 +238,10 @@
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
   "/\\" > "op &"
-  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
+  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
   "," > "Pair"
-  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
-  "*" > "HOL.times_class.times" :: "nat => nat => nat"
+  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
+  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
   "$" > "HOLLight.hollight.$"
   "!" > "All"
isabelle