diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/Automata.ML
--- a/src/HOL/Lex/Automata.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Automata.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -8,35 +8,35 @@
 
 Goalw [na2da_def]
  "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
-by(induct_tac "w" 1);
- by(ALLGOALS Asm_simp_tac);
- by(ALLGOALS Blast_tac);
+by (induct_tac "w" 1);
+ by (ALLGOALS Asm_simp_tac);
+ by (ALLGOALS Blast_tac);
 qed_spec_mp "DA_delta_is_lift_NA_delta";
 
 Goalw [DA.accepts_def,NA.accepts_def]
   "NA.accepts A w = DA.accepts (na2da A) w";
-by(simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
-by(simp_tac (simpset() addsimps [na2da_def]) 1);
+by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
+by (simp_tac (simpset() addsimps [na2da_def]) 1);
 qed "NA_DA_equiv";
 
 (*** Direct equivalence of NAe and DA ***)
 
 Goalw [nae2da_def]
  "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
-by(induct_tac "w" 1);
+by (induct_tac "w" 1);
  by (Simp_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
+by (Blast_tac 1);
 qed_spec_mp "espclosure_DA_delta_is_steps";
 
 Goalw [nae2da_def]
  "fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 val lemma = result();
 
 Goalw [NAe.accepts_def,DA.accepts_def]
   "DA.accepts (nae2da A) w = NAe.accepts A w";
-by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
-by(simp_tac (simpset() addsimps [nae2da_def]) 1);
-by(Blast_tac 1);
+by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
+by (simp_tac (simpset() addsimps [nae2da_def]) 1);
+by (Blast_tac 1);
 qed "NAe_DA_equiv";