Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Introduced variants of operators + * ~ constrained to type int
authorberghofe
Mon, 25 Feb 2002 11:27:07 +0100
changeset 12933 b85c62c4e826
parent 12932 3bda5306d262
child 12934 6003b4f916c0
Introduced variants of operators + * ~ constrained to type int (to make SML/NJ happy).
src/HOL/Integ/NatBin.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/NatBin.thy	Mon Feb 25 10:45:22 2002 +0100
+++ b/src/HOL/Integ/NatBin.thy	Mon Feb 25 11:27:07 2002 +0100
@@ -62,6 +62,15 @@
 
 subsection {* Configuration of the code generator *}
 
+ML {*
+infix 7 `*;
+infix 6 `+;
+
+val op `* = op * : int * int -> int;
+val op `+ = op + : int * int -> int;
+val `~ = ~ : int -> int;
+*}
+
 types_code
   "int" ("int")
 
@@ -73,9 +82,9 @@
 consts_code
   "0" :: "int"                  ("0")
   "1" :: "int"                  ("1")
-  "uminus" :: "int => int"      ("~")
-  "op +" :: "int => int => int" ("(_ +/ _)")
-  "op *" :: "int => int => int" ("(_ */ _)")
+  "uminus" :: "int => int"      ("`~")
+  "op +" :: "int => int => int" ("(_ `+/ _)")
+  "op *" :: "int => int => int" ("(_ `*/ _)")
   "neg"                         ("(_ < 0)")
 
 end
isabelle