src/HOL/IMP/Denotation.ML

--- a/src/HOL/IMP/Denotation.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/IMP/Denotation.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -15,11 +15,11 @@
 
 
 goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
-by(Simp_tac 1);
-by(EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
+by (Simp_tac 1);
+by (EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
           stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1,
-	  Simp_tac 1,
-	  IF_UNSOLVED no_tac]);
+          Simp_tac 1,
+          IF_UNSOLVED no_tac]);
 qed "C_While_If";
 
 
@@ -31,7 +31,7 @@
 by (etac evalc.induct 1);
 auto();
 (* while *)
-by(rewtac Gamma_def);
+by (rewtac Gamma_def);
 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
 by (Fast_tac 1);
 by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
@@ -44,8 +44,8 @@
 goal Denotation.thy "!s t. (s,t):C(c) --> <c,s> -c-> t";
 by (com.induct_tac "c" 1);
 
-by(ALLGOALS Full_simp_tac);
-by(ALLGOALS (TRY o Fast_tac));
+by (ALLGOALS Full_simp_tac);
+by (ALLGOALS (TRY o Fast_tac));
 
 (* while *)
 by (strip_tac 1);