src/HOL/Lambda/ParRed.ML

--- a/src/HOL/Lambda/ParRed.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -21,13 +21,13 @@
 (*** beta <= par_beta <= beta^* ***)
 
 goal ParRed.thy "(Var n => t) = (t = Var n)";
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed "par_beta_varL";
 Addsimps [par_beta_varL];
 
 goal ParRed.thy "t => t";
-by(db.induct_tac "t" 1);
-by(ALLGOALS Asm_simp_tac);
+by (db.induct_tac "t" 1);
+by (ALLGOALS Asm_simp_tac);
 qed"par_beta_refl";
 Addsimps [par_beta_refl];
 (* AddSIs [par_beta_refl]; causes search to blow up *)
@@ -50,21 +50,21 @@
 (*** => ***)
 
 goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
-by(db.induct_tac "t" 1);
-by(ALLGOALS(fast_tac (!claset addss (!simpset))));
+by (db.induct_tac "t" 1);
+by (ALLGOALS(fast_tac (!claset addss (!simpset))));
 qed_spec_mp "par_beta_lift";
 Addsimps [par_beta_lift];
 
 goal ParRed.thy
   "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
-by(db.induct_tac "t" 1);
+by (db.induct_tac "t" 1);
   by(asm_simp_tac (addsplit(!simpset)) 1);
  by(strip_tac 1);
  bes par_beta_cases 1;
   by(Asm_simp_tac 1);
  by(asm_simp_tac (!simpset addsimps [subst_subst RS sym]) 1);
  by(fast_tac (!claset addSIs [par_beta_lift] addss (!simpset)) 1);
-by(fast_tac (!claset addss (!simpset)) 1);
+by (fast_tac (!claset addss (!simpset)) 1);
 qed_spec_mp "par_beta_subst";
 
 (*** Confluence (directly) ***)
@@ -72,14 +72,14 @@
 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
 by (rtac (impI RS allI RS allI) 1);
 by (etac par_beta.induct 1);
-by(ALLGOALS(fast_tac (!claset addSIs [par_beta_subst])));
+by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst])));
 qed "diamond_par_beta";
 
 
 (*** cd ***)
 
 goal ParRed.thy "!t. s => t --> t => cd s";
-by(db.induct_tac "s" 1);
+by (db.induct_tac "s" 1);
   by(Simp_tac 1);
  be rev_mp 1;
  by(db.induct_tac "db1" 1);
@@ -89,10 +89,10 @@
 (*** Confluence (via cd) ***)
 
 goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by(fast_tac (HOL_cs addIs [par_beta_cd]) 1);
+by (fast_tac (HOL_cs addIs [par_beta_cd]) 1);
 qed "diamond_par_beta2";
 
 goal ParRed.thy "confluent(beta)";
-by(fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence,
+by (fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence,
                            par_beta_subset_beta,beta_subset_par_beta]) 1);
 qed"beta_confluent";