src/HOL/Product_Type.thy
changeset 34886 873c31d9f10d
parent 33959 2afc55e8ed27
child 34900 9b12b0824bfe
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jan 12 13:36:01 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Jan 13 08:56:15 2010 +0100
     1.3 @@ -99,6 +99,7 @@
     1.4    (SML "unit")
     1.5    (OCaml "unit")
     1.6    (Haskell "()")
     1.7 +  (Scala "Unit")
     1.8  
     1.9  code_instance unit :: eq
    1.10    (Haskell -)
    1.11 @@ -110,6 +111,7 @@
    1.12    (SML "()")
    1.13    (OCaml "()")
    1.14    (Haskell "()")
    1.15 +  (Scala "()")
    1.16  
    1.17  code_reserved SML
    1.18    unit
    1.19 @@ -117,6 +119,9 @@
    1.20  code_reserved OCaml
    1.21    unit
    1.22  
    1.23 +code_reserved Scala
    1.24 +  Unit
    1.25 +
    1.26  
    1.27  subsection {* Pairs *}
    1.28  
    1.29 @@ -995,6 +1000,7 @@
    1.30    (SML infix 2 "*")
    1.31    (OCaml infix 2 "*")
    1.32    (Haskell "!((_),/ (_))")
    1.33 +  (Scala "!((_),/ (_))")
    1.34  
    1.35  code_instance * :: eq
    1.36    (Haskell -)
    1.37 @@ -1006,6 +1012,7 @@
    1.38    (SML "!((_),/ (_))")
    1.39    (OCaml "!((_),/ (_))")
    1.40    (Haskell "!((_),/ (_))")
    1.41 +  (Scala "!((_),/ (_))")
    1.42  
    1.43  code_const fst and snd
    1.44    (Haskell "fst" and "snd")