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 35267 8dfd816713c6
parent 34974 18b41bba42b5
child 37387 3581483cca6c 
--- a/src/HOL/Import/HOLLight/hollight.imp	Fri Feb 19 14:47:00 2010 +0100
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Feb 19 14:47:01 2010 +0100
@@ -238,10 +238,10 @@
   "<=" > "HOLLight.hollight.<="
   "<" > "HOLLight.hollight.<"
   "/\\" > "op &"
-  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
+  "-" > "Groups.minus" :: "nat => nat => nat"
   "," > "Pair"
-  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
-  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
+  "+" > "Groups.plus" :: "nat => nat => nat"
+  "*" > "Groups.times" :: "nat => nat => nat"
   "$" > "HOLLight.hollight.$"
   "!" > "All"
isabelle