Trivial spacing corrections
authorlcp
Fri Nov 19 11:35:59 1993 +0100 (1993-11-19)
changeset 132b5704e45d2d2
parent 131 bb0caac13eff
child 133 2322fd6d57a1
Trivial spacing corrections
src/FOL/ex/Nat.ML
src/FOL/ex/nat.ML
src/Modal/S4.thy
src/Modal/s4.thy
     1.1 --- a/src/FOL/ex/Nat.ML	Fri Nov 19 11:34:31 1993 +0100
     1.2 +++ b/src/FOL/ex/Nat.ML	Fri Nov 19 11:35:59 1993 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  by (resolve_tac [rec_Suc] 1);
     1.5  val add_Suc = result();
     1.6  
     1.7 -val add_ss = FOL_ss  addsimps  [add_0, add_Suc];
     1.8 +val add_ss = FOL_ss addsimps [add_0, add_Suc];
     1.9  
    1.10  goal Nat.thy "(k+m)+n = k+(m+n)";
    1.11  by (res_inst_tac [("n","k")] induct 1);
     2.1 --- a/src/FOL/ex/nat.ML	Fri Nov 19 11:34:31 1993 +0100
     2.2 +++ b/src/FOL/ex/nat.ML	Fri Nov 19 11:35:59 1993 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4  by (resolve_tac [rec_Suc] 1);
     2.5  val add_Suc = result();
     2.6  
     2.7 -val add_ss = FOL_ss  addsimps  [add_0, add_Suc];
     2.8 +val add_ss = FOL_ss addsimps [add_0, add_Suc];
     2.9  
    2.10  goal Nat.thy "(k+m)+n = k+(m+n)";
    2.11  by (res_inst_tac [("n","k")] induct 1);
     3.1 --- a/src/Modal/S4.thy	Fri Nov 19 11:34:31 1993 +0100
     3.2 +++ b/src/Modal/S4.thy	Fri Nov 19 11:35:59 1993 +0100
     3.3 @@ -21,10 +21,11 @@
     3.4  
     3.5    boxR
     3.6     "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  \
     3.7 -\               $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
     3.8 +\           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
     3.9    boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    3.10 +
    3.11    diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    3.12    diaL
    3.13     "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  \
    3.14 -\               $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    3.15 +\           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    3.16  end
     4.1 --- a/src/Modal/s4.thy	Fri Nov 19 11:34:31 1993 +0100
     4.2 +++ b/src/Modal/s4.thy	Fri Nov 19 11:35:59 1993 +0100
     4.3 @@ -21,10 +21,11 @@
     4.4  
     4.5    boxR
     4.6     "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  \
     4.7 -\               $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
     4.8 +\           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
     4.9    boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
    4.10 +
    4.11    diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
    4.12    diaL
    4.13     "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  \
    4.14 -\               $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    4.15 +\           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
    4.16  end