--- a/src/Modal/s4.thy Fri Nov 19 11:34:31 1993 +0100
+++ b/src/Modal/s4.thy Fri Nov 19 11:35:59 1993 +0100
@@ -21,10 +21,11 @@
boxR
"[| $E |L> $E'; $F |R> $F'; $G |R> $G'; \
-\ $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G"
+\ $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G"
boxL "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G"
+
diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G"
diaL
"[| $E |L> $E'; $F |L> $F'; $G |R> $G'; \
-\ $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"
+\ $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"
end