src/HOL/Lex/NA.ML
changeset 6301 08245f5a436d
parent 5323 028e00595280
     1.1 --- a/src/HOL/Lex/NA.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Lex/NA.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -7,23 +7,23 @@
     1.4  Goal
     1.5   "steps A (v@w) = steps A w  O  steps A v";
     1.6  by (induct_tac "v" 1);
     1.7 -by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
     1.8 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
     1.9  qed "steps_append";
    1.10  Addsimps [steps_append];
    1.11  
    1.12  Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
    1.13 -by(rtac (steps_append RS equalityE) 1);
    1.14 -by(Blast_tac 1);
    1.15 +by (rtac (steps_append RS equalityE) 1);
    1.16 +by (Blast_tac 1);
    1.17  qed "in_steps_append";
    1.18  AddIffs [in_steps_append];
    1.19  
    1.20  Goal
    1.21   "!p. delta A w p = {q. (p,q) : steps A w}";
    1.22 -by(induct_tac "w" 1);
    1.23 -by(auto_tac (claset(), simpset() addsimps [step_def]));
    1.24 +by (induct_tac "w" 1);
    1.25 +by (auto_tac (claset(), simpset() addsimps [step_def]));
    1.26  qed_spec_mp "delta_conv_steps";
    1.27  
    1.28  Goalw [accepts_def]
    1.29   "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
    1.30 -by(simp_tac (simpset() addsimps [delta_conv_steps]) 1);
    1.31 +by (simp_tac (simpset() addsimps [delta_conv_steps]) 1);
    1.32  qed "accepts_conv_steps";