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.
added explicit serialization for int equality
authorhaftmann
Thu, 06 Apr 2006 16:12:57 +0200
changeset 19348 f2283f334e42
parent 19347 e2e709f3f955
child 19349 36e537f89585
added explicit serialization for int equality
src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/IntDef.thy	Thu Apr 06 16:11:30 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Apr 06 16:12:57 2006 +0200
@@ -915,6 +915,9 @@
   "uminus :: int \<Rightarrow> int"
     ml (target_atom "~")
     haskell (target_atom "negate")
+  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
+    ml (infixl 6 "=")
+    haskell (infixl 4 "==")
   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
     ml (infix 6 "<")
     haskell (infix 4 "<")
isabelle