src/HOL/Lex/AutoChopper.ML

    by (Simp_tac 1);
   by (res_inst_tac [("P","%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (delta A as (next A a st)))")] exE 1);
    by (asm_simp_tac HOL_ss 1);
   by (res_inst_tac [("x","x")] exI 1);
   by (Asm_simp_tac 1);
-  by(rtac allI 1);
-  by(case_tac "as" 1);
+  by (rtac allI 1);
+  by (case_tac "as" 1);
    by (Asm_simp_tac 1);
   by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
  by (strip_tac 1);
  by (res_inst_tac [("f","%k. a#k")] ex_special 1);
  by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
   by (Simp_tac 1);
  by (res_inst_tac [("P","%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (delta A as (next A a st)))")] exE 1);
   by (asm_simp_tac HOL_ss 1);
  by (res_inst_tac [("x","x")] exI 1);
  by (Asm_simp_tac 1);
- by(rtac allI 1);
- by(case_tac "as" 1);
+ by (rtac allI 1);
+ by (case_tac "as" 1);
   by (Asm_simp_tac 1);
  by (asm_simp_tac (simpset() addcongs[conj_cong]) 1);
 by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (res_inst_tac [("x","[a]")] exI 1);
 by (rtac conjI 1);
  by (subgoal_tac "r @ [a] ~= []" 1);
   by (Fast_tac 1);
  by (Simp_tac 1);
-by(rtac allI 1);
-by(case_tac "as" 1);
+by (rtac allI 1);
+by (case_tac "as" 1);
  by (Asm_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [acc_prefix_def] addcongs[conj_cong]) 1);
 by (etac thin_rl 1); (* speed up *)
 by (Fast_tac 1);
 qed_spec_mp "step2_e";