src/HOL/Product_Type.thy

 
 code_type unit
   (SML "unit")
   (OCaml "unit")
   (Haskell "()")
+  (Scala "Unit")
 
 code_instance unit :: eq
   (Haskell -)
 
 code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"

 
 code_const Unity
   (SML "()")
   (OCaml "()")
   (Haskell "()")
+  (Scala "()")
 
 code_reserved SML
   unit
 
 code_reserved OCaml
   unit
+
+code_reserved Scala
+  Unit
 
 
 subsection {* Pairs *}
 
 subsubsection {* Product type, basic operations and concrete syntax *}

 
 code_type *
   (SML infix 2 "*")
   (OCaml infix 2 "*")
   (Haskell "!((_),/ (_))")
+  (Scala "!((_),/ (_))")
 
 code_instance * :: eq
   (Haskell -)
 
 code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"

 
 code_const Pair
   (SML "!((_),/ (_))")
   (OCaml "!((_),/ (_))")
   (Haskell "!((_),/ (_))")
+  (Scala "!((_),/ (_))")
 
 code_const fst and snd
   (Haskell "fst" and "snd")
 
 types_code