src/HOL/List.ML

--- a/src/HOL/List.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/List.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -49,8 +49,8 @@
 Addsimps [lists_Int_eq];
 
 Goal "(xs@ys : lists A) = (xs : lists A & ys : lists A)";
-by(induct_tac "xs" 1);
-by(Auto_tac);
+by (induct_tac "xs" 1);
+by (Auto_tac);
 qed "append_in_lists_conv";
 AddIffs [append_in_lists_conv];
 
@@ -725,7 +725,7 @@
 qed_spec_mp "set_update_subset_insert";
 
 Goal "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A";
-by(fast_tac (claset() addSDs [set_update_subset_insert RS subsetD]) 1);
+by (fast_tac (claset() addSDs [set_update_subset_insert RS subsetD]) 1);
 qed "set_update_subsetI";
 
 (** last & butlast **)