src/HOL/Lex/AutoChopper.ML

 Addsimps [Let_def];
 
 goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 val accept_not_Nil = result() repeat_RS spec;
 Addsimps [accept_not_Nil];
 
 goal AutoChopper.thy
 "!st us. acc xs st [] us ([],ys) A = ([], zs) --> \
 \        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
 by (list.induct_tac "xs" 1);
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 by (strip_tac 1);
 by (rtac conjI 1);
 by (Fast_tac 1);
 by (simp_tac (simpset() addsimps [prefix_Cons] addcongs [conj_cong]) 1);
 by (strip_tac 1);

 goal AutoChopper.thy
 "! r erk l rst st ys yss zs::'a list. \
 \    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
 \    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
 by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
+by (Asm_simp_tac 1);
 by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
 by (rename_tac "vss lrst" 1);  
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 by (res_inst_tac[("xs","vss")] list_eq_cases 1);
  by (hyp_subst_tac 1);
  by (Simp_tac 1);
  by (fast_tac (claset() addSDs [no_acc]) 1);
 by (hyp_subst_tac 1);
-by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (Asm_simp_tac 1);
 val step2_a = (result() repeat_RS spec) RS mp;
 
 
 goal AutoChopper.thy
  "! st erk r l rest ys yss zs.\
 \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
 \     (if acc_prefix A st xs \
 \      then ys ~= [] \
 \      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
- by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (Simp_tac 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
+ by (Fast_tac 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 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);

  "! st erk r l rest ys yss zs. \
 \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
 \     (if acc_prefix A st xs                   \
 \      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() addsplits [expand_if]) 1);
-by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
- by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (Simp_tac 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
+ by (Fast_tac 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 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 (Asm_simp_tac 1);

  "! st erk r l rest ys yss zs. \
 \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
 \     (if acc_prefix A st xs       \
 \      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
 \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
-by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
- by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (Simp_tac 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
+ by (Fast_tac 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 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 (etac exE 1);
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
 by (rtac trans 1);
  by (etac step2_a 1);
-by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Simp_tac 1);
 val step2_d = (result() repeat_RS spec) RS mp;
 
 Delsimps [split_paired_All];
 goal AutoChopper.thy 
 "! st erk r p ys yss zs. \
 \  acc xs st erk r p A = (ys#yss, zs) --> \
 \  (if acc_prefix A st xs  \
 \   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() addsplits [expand_if]) 1);
-by (list.induct_tac "xs" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
- by (Fast_tac 1);
-by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
+by (Simp_tac 1);
+by (list.induct_tac "xs" 1);
+ by (simp_tac (simpset() addcongs [conj_cong]) 1);
+ by (Fast_tac 1);
+by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
 by (strip_tac 1);
 by (case_tac "acc_prefix A (next A st a) list" 1);
  by (rtac conjI 1);
   by (strip_tac 1);
   by (res_inst_tac [("f","%k. a#k")] ex_special 1);

                        Chopper.is_longest_prefix_chopper_def]
  "is_auto_chopper(auto_chopper)";
 by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
  by (rtac mp 1);
   by (etac step2_b 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 by (rtac conjI 1);
  by (rtac mp 1);
   by (etac step2_c 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (rtac conjI 1);
- by (asm_simp_tac (simpset() addsimps [step2_a] addsplits [expand_if]) 1);
+ by (Simp_tac 1);
+by (rtac conjI 1);
+ by (asm_simp_tac (simpset() addsimps [step2_a]) 1);
 by (rtac conjI 1);
  by (rtac mp 1);
   by (etac step2_d 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 by (rtac mp 1);
  by (etac step2_e 2);
- by (simp_tac (simpset() addsplits [expand_if]) 1);
+ by (Simp_tac 1);
 qed"auto_chopper_is_auto_chopper";