# HG changeset patch
# User haftmann
# Date 1144332777 -7200
# Node ID f2283f334e427566a02882e494bc1d9e701be1ec
# Parent  e2e709f3f9552b803b514be70d5a9ce81bacb85f
added explicit serialization for int equality

diff -r e2e709f3f955 -r f2283f334e42 src/HOL/Integ/IntDef.thy
--- 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 "<")