src/HOL/Lex/AutoChopper.ML

 by (list.induct_tac "xs" 1);
 by (simp_tac (!simpset addcongs [conj_cong]) 1);
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 by(simp_tac (!simpset addsimps [prefix_Cons] addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by(REPEAT(eresolve_tac [conjE,exE] 1));
 by(hyp_subst_tac 1);
 by (Simp_tac 1);
 by (case_tac "zsa = []" 1);
 by (Asm_simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 bind_thm("no_acc", result() RS spec RS spec RS mp);
 
 
 val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
 by (cut_facts_tac [prem] 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val ex_special = result();
 
 
 goal AutoChopper.thy
 "! r erk l rst st ys yss zs::'a list. \

 by(rename_tac "vss lrst" 1);  
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (res_inst_tac[("xs","vss")] list_eq_cases 1);
  by(hyp_subst_tac 1);
  by(Simp_tac 1);
- by (fast_tac (HOL_cs addSDs [no_acc]) 1);
+ by (fast_tac (!claset addSDs [no_acc]) 1);
 by(hyp_subst_tac 1);
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 val step2_a = (result() repeat_RS spec) RS mp;
 
 

 \      then ys ~= [] \
 \      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by(rename_tac "vss lrst" 1);  
 by(Asm_simp_tac 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
  by(Asm_simp_tac 1);
 by (subgoal_tac "r @ [a] ~= []" 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (Simp_tac 1);
 val step2_b = (result() repeat_RS spec) RS mp;
 
 
 goal AutoChopper.thy  

 \      then ? g. ys=r@g & fin A (nexts A st g)  \
 \      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (strip_tac 1);
 by (rtac conjI 1);
  by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
  by(rename_tac "vss lrst" 1);  

   by (strip_tac 1);
   by (res_inst_tac [("f","%k.a#k")] ex_special 1);
   by (Simp_tac 1);
   by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
    by (Simp_tac 1);
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
  by (strip_tac 1);
  by (res_inst_tac [("x","[a]")] exI 1);
  by (Asm_simp_tac 1);
  by (subgoal_tac "r @ [a] ~= []" 1);
   br sym 1;
-  by (fast_tac HOL_cs 1);
+  by (Fast_tac 1);
  by (Simp_tac 1);
 by (strip_tac 1);
 by (res_inst_tac [("f","%k.a#k")] ex_special 1);
 by (Simp_tac 1);
 by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
  by (Simp_tac 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 val step2_c = (result() repeat_RS spec) RS mp;
 
 
 goal AutoChopper.thy
  "! st erk r l rest ys yss zs. \

 \      then acc(flat(yss)@zs)(start A) [] [] ([],flat(yss)@zs) A = (yss,zs) \
 \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by(res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by(rename_tac "vss lrst" 1);  
 by(Asm_simp_tac 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
  by (Asm_simp_tac 1);
 by (subgoal_tac "acc list (start A) [] [] ([],list) A = (yss,zs)" 1);
  by (Asm_simp_tac 2);
  by (subgoal_tac "r@[a] ~= []" 2);
-  by (fast_tac HOL_cs 2);
+  by (Fast_tac 2);
  by (Simp_tac 2);
 by (subgoal_tac "flat(yss) @ zs = list" 1);
  by(hyp_subst_tac 1);
  by(atac 1);
 by (case_tac "yss = []" 1);
  by (Asm_simp_tac 1);
  by (hyp_subst_tac 1);
- by (fast_tac (HOL_cs addSDs [no_acc]) 1);
+ by (fast_tac (!claset addSDs [no_acc]) 1);
 by (etac ((neq_Nil_conv RS iffD1) RS exE) 1);
 by (etac exE 1);
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
 by (rtac trans 1);

 \   then ? g.ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
 \   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
  br conjI 1;
   by (strip_tac 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 HOL_cs 1);
+  by (Fast_tac 1);
  by (Simp_tac 1);
 by (rtac list_cases 1);
  by (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 HOL_cs 1);
+by (Fast_tac 1);
 val step2_e = (result() repeat_RS spec) RS mp;
 Addsimps[split_paired_All];
 
 goalw AutoChopper.thy [accepts_def, is_auto_chopper_def, auto_chopper_def,
                        Chopper.is_longest_prefix_chopper_def]

  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (rtac conjI 1);
  br mp 1;
   be step2_c 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
- by (fast_tac HOL_cs 1);
+ by (Fast_tac 1);
 by (rtac conjI 1);
  by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
 by (rtac conjI 1);
  br mp 1;
   be step2_d 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (rtac mp 1);
  be step2_e 2;
  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed"auto_chopper_is_auto_chopper";