src/HOLCF/Tr2.thy

 
 Tr2 = Tr1 +
 
 consts
 	"@cifte"	:: "tr=>'c=>'c=>'c"
-                             ("(3If _/ (then _/ else _) fi)" [60,60,60] 60)
+                             ("(3If _/ (then _/ else _) fi)" 60)
 	"Icifte"        :: "tr->'c->'c->'c"
 
-	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [61,60] 60)
+	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [36,35] 35)
 	"cop @andalso"	:: "tr -> tr -> tr" ("trand")
-	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [61,60] 60)
+	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
 	"cop @orelse"	:: "tr -> tr -> tr" ("tror")
 
+        "neg"           :: "tr -> tr"
 
 rules
 
   ifte_def    "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
   andalso_def "trand == (LAM t1 t2.tr_when[t2][FF][t1])"
   orelse_def  "tror  == (LAM t1 t2.tr_when[TT][t2][t1])"
-
+  neg_def     "neg == (LAM t. tr_when[FF][TT][t])"
 
 end
 
 ML