# HG changeset patch
# User haftmann
# Date 1190747316 -7200
# Node ID 56ba87ec8d31acea976bd6f9a9e0f23bda0ec125
# Parent  483f0a64271f32d4b0bf60768b69bee586e5f9e7
rudimentary support for Haskell

diff -r 483f0a64271f -r 56ba87ec8d31 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