# HG changeset patch
# User lcp
# Date 753705359 -3600
# Node ID b5704e45d2d23817fadad5c2cffe63c35ec12b26
# Parent  bb0caac13effaeac96bbc06d9404235a06954b52
Trivial spacing corrections

diff -r bb0caac13eff -r b5704e45d2d2 src/FOL/ex/Nat.ML
--- a/src/FOL/ex/Nat.ML	Fri Nov 19 11:34:31 1993 +0100
+++ b/src/FOL/ex/Nat.ML	Fri Nov 19 11:35:59 1993 +0100
@@ -43,7 +43,7 @@
 by (resolve_tac [rec_Suc] 1);
 val add_Suc = result();
 
-val add_ss = FOL_ss  addsimps  [add_0, add_Suc];
+val add_ss = FOL_ss addsimps [add_0, add_Suc];
 
 goal Nat.thy "(k+m)+n = k+(m+n)";
 by (res_inst_tac [("n","k")] induct 1);
diff -r bb0caac13eff -r b5704e45d2d2 src/FOL/ex/nat.ML
--- a/src/FOL/ex/nat.ML	Fri Nov 19 11:34:31 1993 +0100
+++ b/src/FOL/ex/nat.ML	Fri Nov 19 11:35:59 1993 +0100
@@ -43,7 +43,7 @@
 by (resolve_tac [rec_Suc] 1);
 val add_Suc = result();
 
-val add_ss = FOL_ss  addsimps  [add_0, add_Suc];
+val add_ss = FOL_ss addsimps [add_0, add_Suc];
 
 goal Nat.thy "(k+m)+n = k+(m+n)";
 by (res_inst_tac [("n","k")] induct 1);
diff -r bb0caac13eff -r b5704e45d2d2 src/Modal/S4.thy
--- 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
diff -r bb0caac13eff -r b5704e45d2d2 src/Modal/s4.thy
--- 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