| changeset 28346 | b8390cd56b8f |
| parent 28090 | 29af3c712d2b |
| child 28562 | 4e74209f113e |
--- a/src/HOL/Library/Code_Message.thy Wed Sep 24 19:39:25 2008 +0200 +++ b/src/HOL/Library/Code_Message.thy Thu Sep 25 09:28:03 2008 +0200 @@ -50,7 +50,7 @@ code_instance message_string :: eq (Haskell -) -code_const "op = \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool" +code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool" (SML "!((_ : string) = _)") (OCaml "!((_ : string) = _)") (Haskell infixl 4 "==")