# HG changeset patch
# User haftmann
# Date 1262957657 -3600
# Node ID 25ff5e139a1dc9402727208caac34715830800de
# Parent  6cd289eca3e4bbc993f3d51e88f5265fdcca2a6e
boolean operators for scala

diff -r 6cd289eca3e4 -r 25ff5e139a1d src/HOL/HOL.thy
--- 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