Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trivial spacing corrections
authorlcp
Fri, 19 Nov 1993 11:35:59 +0100
changeset 132 b5704e45d2d2
parent 131 bb0caac13eff
child 133 2322fd6d57a1
Trivial spacing corrections
src/FOL/ex/Nat.ML file | annotate | diff | comparison | revisions
src/FOL/ex/nat.ML file | annotate | diff | comparison | revisions
src/Modal/S4.thy file | annotate | diff | comparison | revisions
src/Modal/s4.thy file | annotate | diff | comparison | revisions 
--- 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);
--- 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);
--- 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
--- 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