author | haftmann |
Tue, 25 Sep 2007 21:08:36 +0200 | |
changeset 24717 | 56ba87ec8d31 |
parent 24716 | 483f0a64271f |
child 24718 | 16b11ba36350 |
--- 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