# HG changeset patch
# User haftmann
# Date 1164631368 -3600
# Node ID da4e5237dda21547c9f54b446ea0d6e06f081d4e
# Parent  d276e7d250176f76f52c676a4706feecde5f4b55
small syntax tuning

diff -r d276e7d25017 -r da4e5237dda2 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Mon Nov 27 13:42:47 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy	Mon Nov 27 13:42:48 2006 +0100
@@ -921,7 +921,7 @@
   (SML "!((_ : IntInf.int) = _)")
   (Haskell infixl 4 "==")
 
-code_const "op <= \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "IntInf.<= (_, _)")
   (Haskell infix 4 "<=")