diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Tr2.ML
--- a/src/HOLCF/Tr2.ML	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Tr2.ML	Mon Jun 20 12:03:16 1994 +0200
@@ -19,13 +19,13 @@
 	]);
 
 val andalso_thms = map prover [
-			"TT andalso y = y",
-			"FF andalso y = FF",
-			"UU andalso y = UU"
+			"(TT andalso y) = y",
+			"(FF andalso y) = FF",
+			"(UU andalso y) = UU"
 			];
 
 val andalso_thms = andalso_thms @ 
- [prove_goalw Tr2.thy [andalso_def] "x andalso TT =  x"
+ [prove_goalw Tr2.thy [andalso_def] "(x andalso TT) =  x"
  (fn prems =>
 	[
 	(res_inst_tac [("p","x")] trE 1),
@@ -45,13 +45,13 @@
 	]);
 
 val orelse_thms = map prover [
-			"TT orelse y  = TT",
-			"FF orelse y =  y",
-			"UU orelse y = UU"
+			"(TT orelse y)  = TT",
+			"(FF orelse y) =  y",
+			"(UU orelse y) = UU"
 			];
 
 val orelse_thms = orelse_thms @ 
- [prove_goalw Tr2.thy [orelse_def] "x orelse FF =  x"
+ [prove_goalw Tr2.thy [orelse_def] "(x orelse FF) =  x"
  (fn prems =>
 	[
 	(res_inst_tac [("p","x")] trE 1),
@@ -62,6 +62,22 @@
 
 
 (* ------------------------------------------------------------------------ *) 
+(* lemmas about neg                                                         *) 
+(* ------------------------------------------------------------------------ *)
+
+fun prover s =  prove_goalw Tr2.thy [neg_def] s
+ (fn prems =>
+	[
+	(simp_tac (ccc1_ss addsimps tr_when) 1)
+	]);
+
+val neg_thms = map prover [
+			"neg[TT] = FF",
+			"neg[FF] = TT",
+			"neg[UU] = UU"
+			];
+
+(* ------------------------------------------------------------------------ *) 
 (* lemmas about If_then_else_fi                                             *) 
 (* ------------------------------------------------------------------------ *)