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/Generate-HOL/GenHOL4Base.thy
changeset 19233 77ca20b0ed77
parent 17628 f4e2587bc7a5
child 19277 f7602e74d948 
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Mar 10 15:33:48 2006 +0100
@@ -182,9 +182,9 @@
   ">="         > HOL4Compat.nat_ge
   FUNPOW       > HOL4Compat.FUNPOW
   "<="         > "op <="          :: "[nat,nat]=>bool"
-  "+"          > "op +"           :: "[nat,nat]=>nat"
-  "*"          > "op *"           :: "[nat,nat]=>nat"
-  "-"          > "op -"           :: "[nat,nat]=>nat"
+  "+"          > "HOL.plus"       :: "[nat,nat]=>nat"
+  "*"          > "HOL.times"      :: "[nat,nat]=>nat"
+  "-"          > "HOL.minus"      :: "[nat,nat]=>nat"
   MIN          > Orderings.min    :: "[nat,nat]=>nat"
   MAX          > Orderings.max    :: "[nat,nat]=>nat"
   DIV          > "Divides.op div" :: "[nat,nat]=>nat"
isabelle