--- a/src/HOLCF/Tr2.thy Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Tr2.thy Mon Jun 20 12:03:16 1994 +0200
@@ -10,21 +10,22 @@
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