src/HOL/HOL.thy
changeset 34305 25ff5e139a1d
parent 34294 19c1fd52d6c9
child 34873 c6449a41b214
--- a/src/HOL/HOL.thy	Fri Jan 08 14:07:07 2010 +0100
+++ b/src/HOL/HOL.thy	Fri Jan 08 14:34:17 2010 +0100
@@ -1925,9 +1925,9 @@
   (Haskell "True" and "False" and "not"
     and infixl 3 "&&" and infixl 2 "||"
     and "!(if (_)/ then (_)/ else (_))")
-
-code_const True and False
-  (Scala "true" and "false")
+  (Scala "true" and "false" and "'! _"
+    and infixl 3 "&&" and infixl 1 "||"
+    and "!(if ((_))/ (_)/ else (_))")
 
 code_reserved SML
   bool true false not