--- a/src/HOL/String.thy Tue Jan 12 13:36:01 2010 +0100
+++ b/src/HOL/String.thy Wed Jan 13 08:56:15 2010 +0100
@@ -170,14 +170,16 @@
code_reserved SML string
code_reserved OCaml string
+code_reserved Scala string
code_type literal
(SML "string")
(OCaml "string")
(Haskell "String")
+ (Scala "String")
setup {*
- fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
+ fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
*}
code_instance literal :: eq
@@ -187,7 +189,7 @@
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
-
+ (Scala infixl 5 "==")
types_code
"char" ("string")