src/HOL/Product_Type.thy
changeset 34886 873c31d9f10d
parent 33959 2afc55e8ed27
child 34900 9b12b0824bfe
--- a/src/HOL/Product_Type.thy	Tue Jan 12 13:36:01 2010 +0100
+++ b/src/HOL/Product_Type.thy	Wed Jan 13 08:56:15 2010 +0100
@@ -99,6 +99,7 @@
   (SML "unit")
   (OCaml "unit")
   (Haskell "()")
+  (Scala "Unit")
 
 code_instance unit :: eq
   (Haskell -)
@@ -110,6 +111,7 @@
   (SML "()")
   (OCaml "()")
   (Haskell "()")
+  (Scala "()")
 
 code_reserved SML
   unit
@@ -117,6 +119,9 @@
 code_reserved OCaml
   unit
 
+code_reserved Scala
+  Unit
+
 
 subsection {* Pairs *}
 
@@ -995,6 +1000,7 @@
   (SML infix 2 "*")
   (OCaml infix 2 "*")
   (Haskell "!((_),/ (_))")
+  (Scala "!((_),/ (_))")
 
 code_instance * :: eq
   (Haskell -)
@@ -1006,6 +1012,7 @@
   (SML "!((_),/ (_))")
   (OCaml "!((_),/ (_))")
   (Haskell "!((_),/ (_))")
+  (Scala "!((_),/ (_))")
 
 code_const fst and snd
   (Haskell "fst" and "snd")