Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Modal/s4.thy
changeset 132 b5704e45d2d2
parent 0 a5a9c433f639 
--- 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
isabelle