# HG changeset patch
# User haftmann
# Date 1175264341 -7200
# Node ID 70f5cf8a0fadac11c438f4c98abb34fee32272bb
# Parent  e52f5400e331c89dff0d57e3fe877e8fe57c89a9
equality on strings

diff -r e52f5400e331 -r 70f5cf8a0fad src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Fri Mar 30 16:19:00 2007 +0200
+++ b/src/HOL/Library/MLString.thy	Fri Mar 30 16:19:01 2007 +0200
@@ -67,14 +67,17 @@
 
 code_reserved SML string explode
 
+code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
+  (SML "!((_ : string) = _)")
+  (Haskell infixl 4 "==")
+
+code_instance ml_string :: eq (Haskell -)
+
 text {* disable something ugly *}
 
 code_const "ml_string_rec" and "ml_string_case" and "size \<Colon> ml_string \<Rightarrow> nat"
   (SML "!((_); (_); raise Fail \"ml'_string'_rec\")"
     and "!((_); (_); raise Fail \"ml'_string'_case\")"
     and "!((_); raise Fail \"size'_ml'_string\")")
-  (OCaml "!((_); (_); failwith \"ml'_string'_rec\")"
-    and "!((_); (_); failwith \"ml'_string'_case\")"
-    and "!((_); failwith \"size'_ml'_string\")")
 
 end