src/HOL/Library/ML_String.thy

--- a/src/HOL/Library/ML_String.thy	Tue Sep 25 21:08:35 2007 +0200
+++ b/src/HOL/Library/ML_String.thy	Tue Sep 25 21:08:36 2007 +0200
@@ -47,6 +47,7 @@
 
 code_type ml_string
   (SML "string")
+  (Haskell "String")
 
 setup {*
 let
@@ -65,9 +66,16 @@
 end
 *}
 
+code_const STR
+  (Haskell "_")
+
 code_reserved SML string
 
+code_instance ml_string :: eq
+  (Haskell -)
+
 code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
+  (Haskell infixl 4 "==")
 
 end