src/HOL/simpdata.ML

--- a/src/HOL/simpdata.ML	Fri Jan 07 11:04:15 2000 +0100
+++ b/src/HOL/simpdata.ML	Fri Jan 07 11:06:03 2000 +0100
@@ -232,8 +232,8 @@
 prove "imp_disjL" "((P|Q) --> R) = ((P-->R)&(Q-->R))";
 
 (*These two are specialized, but imp_disj_not1 is useful in Auth/Yahalom.ML*)
-prove "imp_disj_not1" "((P --> Q | R)) = (~Q --> P --> R)";
-prove "imp_disj_not2" "((P --> Q | R)) = (~R --> P --> Q)";
+prove "imp_disj_not1" "(P --> Q | R) = (~Q --> P --> R)";
+prove "imp_disj_not2" "(P --> Q | R) = (~R --> P --> Q)";
 
 prove "imp_disj1" "((P-->Q)|R) = (P--> Q|R)";
 prove "imp_disj2" "(Q|(P-->R)) = (P--> Q|R)";