setloop split_tac -> addsplits
authornipkow
Fri Oct 17 15:25:12 1997 +0200 (1997-10-17)
changeset 3919c036caebfc75
parent 3918 94e0fdcb7b91
child 3920 176d617a8ba8
setloop split_tac -> addsplits
src/HOL/Arith.ML
src/HOL/Auth/Event.ML
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/IMP/Hoare.ML
src/HOL/IOA/IOA.ML
src/HOL/IOA/Solve.ML
src/HOL/Induct/Com.ML
src/HOL/Induct/LFilter.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/Mutil.ML
src/HOL/Induct/Perm.ML
src/HOL/Induct/PropLog.ML
src/HOL/Induct/SList.ML
src/HOL/Integ/Bin.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Lambda.ML
src/HOL/Lex/AutoChopper.ML
src/HOL/List.ML
src/HOL/MiniML/Generalize.ML
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/Maybe.ML
src/HOL/MiniML/MiniML.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/W.ML
src/HOL/Prod.ML
src/HOL/Set.ML
src/HOL/Subst/Subst.ML
src/HOL/Subst/Unifier.ML
src/HOL/Subst/Unify.ML
src/HOL/W0/I.ML
src/HOL/W0/Maybe.ML
src/HOL/W0/Type.ML
src/HOL/W0/W.ML
src/HOL/WF.ML
src/HOL/equalities.ML
src/HOL/ex/Fib.ML
src/HOL/ex/InSort.ML
src/HOL/ex/Primes.ML
src/HOL/ex/Qsort.ML
src/HOL/ex/Recdef.ML
src/HOL/ex/Sorting.ML
src/HOL/ex/set.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Oct 17 15:23:14 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Oct 17 15:25:12 1997 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  AddIffs [pred_le];
     1.5  
     1.6  goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
     1.7 -by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
     1.8 +by(simp_tac (!simpset addsplits [expand_nat_case]) 1);
     1.9  qed_spec_mp "pred_le_mono";
    1.10  
    1.11  goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
    1.12 @@ -434,7 +434,7 @@
    1.13  
    1.14  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.15  by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
    1.16 -                    setloop (split_tac [expand_if])) 1);
    1.17 +                       addsplits [expand_if]) 1);
    1.18  qed "if_Suc_diff_n";
    1.19  
    1.20  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
     2.1 --- a/src/HOL/Auth/Event.ML	Fri Oct 17 15:23:14 1997 +0200
     2.2 +++ b/src/HOL/Auth/Event.ML	Fri Oct 17 15:25:12 1997 +0200
     2.3 @@ -46,7 +46,7 @@
     2.4  qed "spies_subset_spies_Says";
     2.5  
     2.6  goal thy "spies evs <= spies (Notes A X # evs)";
     2.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
     2.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
     2.9  by (Fast_tac 1);
    2.10  qed "spies_subset_spies_Notes";
    2.11  
    2.12 @@ -54,14 +54,14 @@
    2.13  goal thy "Says A B X : set evs --> X : spies evs";
    2.14  by (induct_tac "evs" 1);
    2.15  by (ALLGOALS (asm_simp_tac
    2.16 -	      (!simpset setloop split_tac [expand_event_case, expand_if])));
    2.17 +	      (!simpset addsplits [expand_event_case, expand_if])));
    2.18  qed_spec_mp "Says_imp_spies";
    2.19  
    2.20  (*Spy sees Notes of bad agents*)
    2.21  goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
    2.22  by (induct_tac "evs" 1);
    2.23  by (ALLGOALS (asm_simp_tac
    2.24 -	      (!simpset setloop split_tac [expand_event_case, expand_if])));
    2.25 +	      (!simpset addsplits [expand_event_case, expand_if])));
    2.26  qed_spec_mp "Notes_imp_spies";
    2.27  
    2.28  (*Use with addSEs to derive contradictions from old Says events containing
    2.29 @@ -80,7 +80,7 @@
    2.30  by (induct_tac "evs" 1);
    2.31  by (ALLGOALS (asm_simp_tac
    2.32  	      (!simpset addsimps [parts_insert_spies]
    2.33 -	                setloop split_tac [expand_event_case, expand_if])));
    2.34 +	                addsplits [expand_event_case, expand_if])));
    2.35  by (ALLGOALS Blast_tac);
    2.36  qed "parts_spies_subset_used";
    2.37  
    2.38 @@ -91,7 +91,7 @@
    2.39  by (induct_tac "evs" 1);
    2.40  by (ALLGOALS (asm_simp_tac
    2.41  	      (!simpset addsimps [parts_insert_spies]
    2.42 -	                setloop split_tac [expand_event_case, expand_if])));
    2.43 +	                addsplits [expand_event_case, expand_if])));
    2.44  by (ALLGOALS Blast_tac);
    2.45  bind_thm ("initState_into_used", impOfSubs (result()));
    2.46  
     3.1 --- a/src/HOL/Auth/Message.ML	Fri Oct 17 15:23:14 1997 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Fri Oct 17 15:25:12 1997 +0200
     3.3 @@ -899,7 +899,7 @@
     3.4         (REPEAT o CHANGED)
     3.5             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
     3.6         (*...allowing further simplifications*)
     3.7 -       simp_tac (!simpset setloop split_tac [expand_if]) 1,
     3.8 +       simp_tac (!simpset addsplits [expand_if]) 1,
     3.9         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    3.10         DEPTH_SOLVE 
    3.11           (Fake_insert_simp_tac 1
     4.1 --- a/src/HOL/Auth/NS_Public.ML	Fri Oct 17 15:23:14 1997 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public.ML	Fri Oct 17 15:25:12 1997 +0200
     4.3 @@ -124,7 +124,7 @@
     4.4  fun analz_induct_tac i = 
     4.5      etac ns_public.induct i   THEN
     4.6      ALLGOALS (asm_simp_tac 
     4.7 -              (!simpset setloop split_tac [expand_if]));
     4.8 +              (!simpset addsplits [expand_if]));
     4.9  
    4.10  
    4.11  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
     5.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Oct 17 15:23:14 1997 +0200
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Oct 17 15:25:12 1997 +0200
     5.3 @@ -126,8 +126,7 @@
     5.4  (*Tactic for proving secrecy theorems*)
     5.5  fun analz_induct_tac i = 
     5.6      etac ns_public.induct i   THEN
     5.7 -    ALLGOALS (asm_simp_tac 
     5.8 -              (!simpset setloop split_tac [expand_if]));
     5.9 +    ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
    5.10  
    5.11  
    5.12  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
     6.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Oct 17 15:23:14 1997 +0200
     6.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Oct 17 15:25:12 1997 +0200
     6.3 @@ -267,7 +267,7 @@
     6.4  by (ALLGOALS 
     6.5      (asm_simp_tac 
     6.6       (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
     6.7 -               setloop split_tac [expand_if])));
     6.8 +               addsplits [expand_if])));
     6.9  (*Oops*)
    6.10  by (blast_tac (!claset addDs [unique_session_keys]) 5);
    6.11  (*NS3, replay sub-case*) 
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Oct 17 15:23:14 1997 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Oct 17 15:25:12 1997 +0200
     7.3 @@ -339,7 +339,7 @@
     7.4  by (ALLGOALS
     7.5      (asm_simp_tac (!simpset addcongs [conj_cong] 
     7.6                              addsimps [analz_insert_eq, analz_insert_freshK]
     7.7 -                            setloop split_tac [expand_if])));
     7.8 +                            addsplits [expand_if])));
     7.9  (*Oops*)
    7.10  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    7.11  (*OR4*) 
     8.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Oct 17 15:23:14 1997 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Oct 17 15:25:12 1997 +0200
     8.3 @@ -268,7 +268,7 @@
     8.4  by (ALLGOALS
     8.5      (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
     8.6                              addsimps [analz_insert_eq, analz_insert_freshK]
     8.7 -                            setloop split_tac [expand_if])));
     8.8 +                            addsplits [expand_if])));
     8.9  (*Oops*)
    8.10  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    8.11  (*OR4*) 
     9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Fri Oct 17 15:23:14 1997 +0200
     9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Oct 17 15:25:12 1997 +0200
     9.3 @@ -231,7 +231,7 @@
     9.4  by (ALLGOALS
     9.5      (asm_simp_tac (!simpset addcongs [conj_cong] 
     9.6                              addsimps [analz_insert_eq, analz_insert_freshK]
     9.7 -                            setloop split_tac [expand_if])));
     9.8 +                            addsplits [expand_if])));
     9.9  (*Oops*)
    9.10  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    9.11  (*OR4*) 
    10.1 --- a/src/HOL/Auth/Public.ML	Fri Oct 17 15:23:14 1997 +0200
    10.2 +++ b/src/HOL/Auth/Public.ML	Fri Oct 17 15:25:12 1997 +0200
    10.3 @@ -58,7 +58,7 @@
    10.4  by (induct_tac "evs" 1);
    10.5  by (ALLGOALS (asm_simp_tac
    10.6  	      (!simpset addsimps [imageI, spies_Cons]
    10.7 -	                setloop split_tac [expand_event_case, expand_if])));
    10.8 +	                addsplits [expand_event_case, expand_if])));
    10.9  qed_spec_mp "spies_pubK";
   10.10  
   10.11  (*Spy sees private keys of bad agents!*)
   10.12 @@ -66,7 +66,7 @@
   10.13  by (induct_tac "evs" 1);
   10.14  by (ALLGOALS (asm_simp_tac
   10.15  	      (!simpset addsimps [imageI, spies_Cons]
   10.16 -	                setloop split_tac [expand_event_case, expand_if])));
   10.17 +	                addsplits [expand_event_case, expand_if])));
   10.18  qed "Spy_spies_bad";
   10.19  
   10.20  AddIffs [spies_pubK, spies_pubK RS analz.Inj];
   10.21 @@ -114,7 +114,7 @@
   10.22  by (res_inst_tac [("x","0")] exI 1);
   10.23  by (ALLGOALS (asm_simp_tac
   10.24  	      (!simpset addsimps [used_Cons]
   10.25 -			setloop split_tac [expand_event_case, expand_if])));
   10.26 +			addsplits [expand_event_case, expand_if])));
   10.27  by Safe_tac;
   10.28  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
   10.29  by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
   10.30 @@ -160,5 +160,5 @@
   10.31  			rangeI, 
   10.32  			insert_Key_singleton, 
   10.33  			insert_Key_image, Un_assoc RS sym]
   10.34 -              setloop split_tac [expand_if];
   10.35 +              addsplits [expand_if];
   10.36  
    11.1 --- a/src/HOL/Auth/Recur.ML	Fri Oct 17 15:23:14 1997 +0200
    11.2 +++ b/src/HOL/Auth/Recur.ML	Fri Oct 17 15:25:12 1997 +0200
    11.3 @@ -455,7 +455,7 @@
    11.4      (asm_simp_tac
    11.5       (!simpset addsimps [analz_insert_eq, parts_insert_spies, 
    11.6  			 analz_insert_freshK] 
    11.7 -               setloop split_tac [expand_if])));
    11.8 +               addsplits [expand_if])));
    11.9  (*RA4*)
   11.10  by (spy_analz_tac 5);
   11.11  (*RA2*)
    12.1 --- a/src/HOL/Auth/Shared.ML	Fri Oct 17 15:23:14 1997 +0200
    12.2 +++ b/src/HOL/Auth/Shared.ML	Fri Oct 17 15:25:12 1997 +0200
    12.3 @@ -36,7 +36,7 @@
    12.4  by (induct_tac "evs" 1);
    12.5  by (ALLGOALS (asm_simp_tac
    12.6  	      (!simpset addsimps [imageI, spies_Cons]
    12.7 -	                setloop split_tac [expand_event_case, expand_if])));
    12.8 +	                addsplits [expand_event_case, expand_if])));
    12.9  qed "Spy_spies_bad";
   12.10  
   12.11  AddSIs [Spy_spies_bad];
   12.12 @@ -111,7 +111,7 @@
   12.13  by (res_inst_tac [("x","0")] exI 1);
   12.14  by (ALLGOALS (asm_simp_tac
   12.15  	      (!simpset addsimps [used_Cons]
   12.16 -			setloop split_tac [expand_event_case, expand_if])));
   12.17 +			addsplits [expand_event_case, expand_if])));
   12.18  by Safe_tac;
   12.19  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
   12.20  by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
   12.21 @@ -238,7 +238,7 @@
   12.22                           insert_Key_singleton, subset_Compl_range,
   12.23                           Key_not_used, insert_Key_image, Un_assoc RS sym]
   12.24                          @disj_comms)
   12.25 -              setloop split_tac [expand_if];
   12.26 +              addsplits [expand_if];
   12.27  
   12.28  (*Lemma for the trivial direction of the if-and-only-if*)
   12.29  goal thy  
    13.1 --- a/src/HOL/Auth/TLS.ML	Fri Oct 17 15:23:14 1997 +0200
    13.2 +++ b/src/HOL/Auth/TLS.ML	Fri Oct 17 15:25:12 1997 +0200
    13.3 @@ -146,7 +146,7 @@
    13.4      REPEAT (FIRSTGOAL analz_mono_contra_tac)
    13.5      THEN 
    13.6      fast_tac (!claset addss (!simpset)) i THEN
    13.7 -    ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]));
    13.8 +    ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if]));
    13.9  
   13.10  
   13.11  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   13.12 @@ -198,13 +198,13 @@
   13.13      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
   13.14      ALLGOALS (asm_simp_tac 
   13.15                (!simpset addcongs [if_weak_cong]
   13.16 -                        setloop split_tac [expand_if]))  THEN
   13.17 +                        addsplits [expand_if]))  THEN
   13.18      (*Remove instances of pubK B:  the Spy already knows all public keys.
   13.19        Combining the two simplifier calls makes them run extremely slowly.*)
   13.20      ALLGOALS (asm_simp_tac 
   13.21                (!simpset addcongs [if_weak_cong]
   13.22  			addsimps [insert_absorb]
   13.23 -                        setloop split_tac [expand_if]));
   13.24 +                        addsplits [expand_if]));
   13.25  
   13.26  
   13.27  (*** Properties of items found in Notes ***)
    14.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Oct 17 15:23:14 1997 +0200
    14.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Oct 17 15:25:12 1997 +0200
    14.3 @@ -227,7 +227,7 @@
    14.4  by (ALLGOALS
    14.5      (asm_simp_tac 
    14.6       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    14.7 -               setloop split_tac [expand_if])));
    14.8 +               addsplits [expand_if])));
    14.9  (*Oops*)
   14.10  by (blast_tac (!claset addDs [unique_session_keys]) 3);
   14.11  (*YM3*)
   14.12 @@ -499,7 +499,7 @@
   14.13  by (ALLGOALS
   14.14      (asm_simp_tac 
   14.15       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
   14.16 -               setloop split_tac [expand_if])));
   14.17 +               addsplits [expand_if])));
   14.18  (*Prove YM3 by showing that no NB can also be an NA*)
   14.19  by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
   14.20  	               addSEs [MPair_parts]
    15.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Oct 17 15:23:14 1997 +0200
    15.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Oct 17 15:25:12 1997 +0200
    15.3 @@ -227,7 +227,7 @@
    15.4  by (ALLGOALS
    15.5      (asm_simp_tac 
    15.6       (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    15.7 -               setloop split_tac [expand_if])));
    15.8 +               addsplits [expand_if])));
    15.9  (*Oops*)
   15.10  by (blast_tac (!claset addDs [unique_session_keys]) 3);
   15.11  (*YM3*)
    16.1 --- a/src/HOL/Divides.ML	Fri Oct 17 15:23:14 1997 +0200
    16.2 +++ b/src/HOL/Divides.ML	Fri Oct 17 15:25:12 1997 +0200
    16.3 @@ -222,7 +222,7 @@
    16.4  goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
    16.5  by (subgoal_tac "k mod 2 < 2" 1);
    16.6  by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2);
    16.7 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
    16.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
    16.9  by (Blast_tac 1);
   16.10  qed "mod2_cases";
   16.11  
    17.1 --- a/src/HOL/Finite.ML	Fri Oct 17 15:23:14 1997 +0200
    17.2 +++ b/src/HOL/Finite.ML	Fri Oct 17 15:25:12 1997 +0200
    17.3 @@ -176,7 +176,7 @@
    17.4   by (Asm_simp_tac 1);
    17.5   by (rtac iffI 1);
    17.6    by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
    17.7 -  by (simp_tac (!simpset setloop (split_tac[expand_split])) 1);
    17.8 +  by (simp_tac (!simpset addsplits [expand_split]) 1);
    17.9   by (etac finite_imageI 1);
   17.10  by (simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
   17.11  by (Auto_tac());
   17.12 @@ -244,7 +244,7 @@
   17.13     by (SELECT_GOAL(safe_tac (!claset))1);
   17.14     by (res_inst_tac [("x","k")] exI 1);
   17.15     by (Asm_simp_tac 1);
   17.16 -  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   17.17 +  by (simp_tac (!simpset addsplits [expand_if]) 1);
   17.18    by (Blast_tac 1);
   17.19   by (dtac sym 1);
   17.20   by (rotate_tac ~1 1);
   17.21 @@ -258,7 +258,7 @@
   17.22    by (SELECT_GOAL(safe_tac (!claset))1);
   17.23    by (res_inst_tac [("x","k")] exI 1);
   17.24    by (Asm_simp_tac 1);
   17.25 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   17.26 + by (simp_tac (!simpset addsplits [expand_if]) 1);
   17.27   by (Blast_tac 1);
   17.28  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
   17.29  by (SELECT_GOAL(safe_tac (!claset))1);
   17.30 @@ -272,7 +272,7 @@
   17.31   by (SELECT_GOAL(safe_tac (!claset))1);
   17.32   by (res_inst_tac [("x","k")] exI 1);
   17.33   by (Asm_simp_tac 1);
   17.34 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   17.35 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   17.36  by (Blast_tac 1);
   17.37  val lemma = result();
   17.38  
   17.39 @@ -330,7 +330,7 @@
   17.40  by (etac finite_induct 1);
   17.41  by (ALLGOALS 
   17.42      (asm_simp_tac (!simpset addsimps [Int_insert_left]
   17.43 -	                    setloop split_tac [expand_if])));
   17.44 +	                    addsplits [expand_if])));
   17.45  qed_spec_mp "card_Un_disjoint";
   17.46  
   17.47  goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
    18.1 --- a/src/HOL/IMP/Hoare.ML	Fri Oct 17 15:23:14 1997 +0200
    18.2 +++ b/src/HOL/IMP/Hoare.ML	Fri Oct 17 15:25:12 1997 +0200
    18.3 @@ -61,13 +61,13 @@
    18.4  (*Not suitable for rewriting: LOOPS!*)
    18.5  goal Hoare.thy "wp (WHILE b DO c) Q s = \
    18.6  \                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
    18.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    18.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    18.9  qed "wp_While_if";
   18.10  
   18.11  goal thy
   18.12    "wp (WHILE b DO c) Q s = \
   18.13  \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
   18.14 -by (simp_tac (!simpset setloop(split_tac[expand_if])) 1);
   18.15 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   18.16  by (rtac iffI 1);
   18.17   by (rtac weak_coinduct 1);
   18.18    by (etac CollectI 1);
    19.1 --- a/src/HOL/IOA/IOA.ML	Fri Oct 17 15:23:14 1997 +0200
    19.2 +++ b/src/HOL/IOA/IOA.ML	Fri Oct 17 15:25:12 1997 +0200
    19.3 @@ -32,7 +32,7 @@
    19.4    by (rtac ext 1);
    19.5    by (exhaust_tac "s(i)" 1);
    19.6    by (Asm_simp_tac 1);
    19.7 -  by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    19.8 +  by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
    19.9  qed "filter_oseq_idemp";
   19.10  
   19.11  goalw IOA.thy [mk_trace_def,filter_oseq_def]
   19.12 @@ -42,7 +42,7 @@
   19.13  \  (mk_trace A s n = Some(a)) =                                   \
   19.14  \   (s(n)=Some(a) & a : externals(asig_of(A)))";
   19.15    by (exhaust_tac "s(n)" 1);
   19.16 -  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   19.17 +  by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   19.18    by (Fast_tac 1);
   19.19  qed "mk_trace_thm";
   19.20  
   19.21 @@ -135,7 +135,7 @@
   19.22  \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
   19.23    by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
   19.24                              ioa_projections)
   19.25 -                  setloop (split_tac [expand_if])) 1);
   19.26 +                  addsplits [expand_if]) 1);
   19.27  qed "trans_of_par4";
   19.28  
   19.29  goal IOA.thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
    20.1 --- a/src/HOL/IOA/Solve.ML	Fri Oct 17 15:23:14 1997 +0200
    20.2 +++ b/src/HOL/IOA/Solve.ML	Fri Oct 17 15:25:12 1997 +0200
    20.3 @@ -78,7 +78,7 @@
    20.4  by (asm_full_simp_tac
    20.5        (!simpset addsimps [executions_def,is_execution_fragment_def,
    20.6                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
    20.7 -                setloop (split_tac[expand_if,expand_option_case])) 1);
    20.8 +                addsplits [expand_if,expand_option_case]) 1);
    20.9  qed"comp1_reachable";
   20.10  
   20.11  
   20.12 @@ -98,7 +98,7 @@
   20.13  by (asm_full_simp_tac
   20.14        (!simpset addsimps [executions_def,is_execution_fragment_def,
   20.15                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
   20.16 -                setloop (split_tac[expand_if,expand_option_case])) 1);
   20.17 +                addsplits [expand_if,expand_option_case]) 1);
   20.18  qed"comp2_reachable";
   20.19  
   20.20  
   20.21 @@ -141,7 +141,7 @@
   20.22  by (Asm_full_simp_tac 2);
   20.23  by (Fast_tac 2);
   20.24  by (simp_tac (!simpset addsimps [conj_disj_distribR] addcongs [conj_cong]
   20.25 -                 setloop (split_tac [expand_if])) 1);
   20.26 +                 addsplits [expand_if]) 1);
   20.27  by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   20.28          asm_full_simp_tac(!simpset addsimps[comp1_reachable,
   20.29                                        comp2_reachable])1));
   20.30 @@ -160,7 +160,7 @@
   20.31  by (asm_full_simp_tac
   20.32        (!simpset addsimps [executions_def,is_execution_fragment_def,
   20.33                            par_def,starts_of_def,trans_of_def,rename_def]
   20.34 -                setloop (split_tac[expand_option_case])) 1);
   20.35 +                addsplits [expand_option_case]) 1);
   20.36  by (best_tac (!claset addSDs [spec] addDs [sym] addss (!simpset)) 1);
   20.37  qed"reachable_rename_ioa";
   20.38  
    21.1 --- a/src/HOL/Induct/Com.ML	Fri Oct 17 15:23:14 1997 +0200
    21.2 +++ b/src/HOL/Induct/Com.ML	Fri Oct 17 15:25:12 1997 +0200
    21.3 @@ -53,7 +53,7 @@
    21.4  
    21.5  goalw thy [assign_def] "s[s x/x] = s";
    21.6  by (rtac ext 1);
    21.7 -by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
    21.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    21.9  qed "assign_triv";
   21.10  
   21.11  Addsimps [assign_same, assign_different, assign_triv];
    22.1 --- a/src/HOL/Induct/LFilter.ML	Fri Oct 17 15:23:14 1997 +0200
    22.2 +++ b/src/HOL/Induct/LFilter.ML	Fri Oct 17 15:25:12 1997 +0200
    22.3 @@ -96,7 +96,7 @@
    22.4  
    22.5  goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
    22.6  by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
    22.7 -                           setloop split_tac[expand_if]) 1);
    22.8 +                           addsplits [expand_if]) 1);
    22.9  qed "find_LCons";
   22.10  
   22.11  
   22.12 @@ -141,7 +141,7 @@
   22.13  goal thy "lfilter p (LCons x l) = \
   22.14  \         (if p x then LCons x (lfilter p l) else lfilter p l)";
   22.15  by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
   22.16 -                           setloop split_tac[expand_if]) 1);
   22.17 +                           addsplits [expand_if]) 1);
   22.18  qed "lfilter_LCons";
   22.19  
   22.20  AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   22.21 @@ -186,7 +186,7 @@
   22.22  
   22.23  goal thy "lfilter p (lfilter p l) = lfilter p l";
   22.24  by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   22.25 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   22.26 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
   22.27  by Safe_tac;
   22.28  (*Cases: p x is true or false*)
   22.29  by (Blast_tac 1);
   22.30 @@ -244,7 +244,7 @@
   22.31  \              ==> l'' = LCons y l' --> \
   22.32  \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
   22.33  by (etac findRel.induct 1);
   22.34 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
   22.35 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   22.36  by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
   22.37  qed_spec_mp "findRel_conj_lfilter";
   22.38  
   22.39 @@ -288,7 +288,7 @@
   22.40  
   22.41  goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
   22.42  by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   22.43 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   22.44 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
   22.45  by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
   22.46  qed "lfilter_conj";
   22.47  
   22.48 @@ -326,7 +326,7 @@
   22.49  
   22.50  goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
   22.51  by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   22.52 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   22.53 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
   22.54  by Safe_tac;
   22.55  by (Blast_tac 1);
   22.56  by (case_tac "lmap f l : Domain (findRel p)" 1);
    23.1 --- a/src/HOL/Induct/LList.ML	Fri Oct 17 15:23:14 1997 +0200
    23.2 +++ b/src/HOL/Induct/LList.ML	Fri Oct 17 15:25:12 1997 +0200
    23.3 @@ -10,7 +10,7 @@
    23.4  
    23.5  (** Simplification **)
    23.6  
    23.7 -simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
    23.8 +simpset := !simpset addsplits [expand_split, expand_sum_case];
    23.9  
   23.10  (*For adding _eqI rules to a simpset; we must remove Pair_eq because
   23.11    it may turn an instance of reflexivity into a conjunction!*)
   23.12 @@ -68,11 +68,11 @@
   23.13  
   23.14  (*UNUSED; obsolete?
   23.15  goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
   23.16 -by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
   23.17 +by (simp_tac (!simpset addsplits [expand_split]) 1);
   23.18  qed "split_UN1";
   23.19  
   23.20  goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
   23.21 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
   23.22 +by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
   23.23  qed "sum_case2_UN1";
   23.24  *)
   23.25  
   23.26 @@ -310,7 +310,7 @@
   23.27  by (rename_tac "y" 1);
   23.28  by (stac prem1 1);
   23.29  by (stac prem2 1);
   23.30 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
   23.31 +by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
   23.32  by (strip_tac 1);
   23.33  by (res_inst_tac [("n", "n")] natE 1);
   23.34  by (rename_tac "m" 2);
    24.1 --- a/src/HOL/Induct/Mutil.ML	Fri Oct 17 15:23:14 1997 +0200
    24.2 +++ b/src/HOL/Induct/Mutil.ML	Fri Oct 17 15:25:12 1997 +0200
    24.3 @@ -94,7 +94,7 @@
    24.4  goalw thy [evnodd_def]
    24.5      "evnodd (insert (i,j) C) b = \
    24.6  \      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
    24.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    24.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    24.9  by (Blast_tac 1);
   24.10  qed "evnodd_insert";
   24.11  
   24.12 @@ -110,7 +110,7 @@
   24.13  by (REPEAT_FIRST assume_tac);
   24.14  (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
   24.15  by (REPEAT (asm_full_simp_tac (!simpset addsimps [less_Suc_eq, mod_Suc] 
   24.16 -                          setloop split_tac [expand_if]) 1
   24.17 +                          addsplits [expand_if]) 1
   24.18             THEN Blast_tac 1));
   24.19  qed "domino_singleton";
   24.20  
    25.1 --- a/src/HOL/Induct/Perm.ML	Fri Oct 17 15:23:14 1997 +0200
    25.2 +++ b/src/HOL/Induct/Perm.ML	Fri Oct 17 15:25:12 1997 +0200
    25.3 @@ -41,7 +41,7 @@
    25.4  goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
    25.5  by (etac perm.induct 1);
    25.6  by (Fast_tac 4);
    25.7 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
    25.8 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    25.9  val perm_mem_lemma = result();
   25.10  
   25.11  bind_thm ("perm_mem", perm_mem_lemma RS mp);
    26.1 --- a/src/HOL/Induct/PropLog.ML	Fri Oct 17 15:23:14 1997 +0200
    26.2 +++ b/src/HOL/Induct/PropLog.ML	Fri Oct 17 15:25:12 1997 +0200
    26.3 @@ -142,7 +142,7 @@
    26.4  goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
    26.5  by (PropLog.pl.induct_tac "p" 1);
    26.6  by (Simp_tac 1);
    26.7 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    26.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    26.9  by (Simp_tac 1);
   26.10  by (Fast_tac 1);
   26.11  qed "hyps_Diff";
   26.12 @@ -152,7 +152,7 @@
   26.13  goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
   26.14  by (PropLog.pl.induct_tac "p" 1);
   26.15  by (Simp_tac 1);
   26.16 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   26.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   26.18  by (Simp_tac 1);
   26.19  by (Fast_tac 1);
   26.20  qed "hyps_insert";
   26.21 @@ -174,7 +174,7 @@
   26.22  
   26.23  goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
   26.24  by (PropLog.pl.induct_tac "p" 1);
   26.25 -by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
   26.26 +by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
   26.27  by (Blast_tac 1);
   26.28  qed "hyps_subset";
   26.29  
    27.1 --- a/src/HOL/Induct/SList.ML	Fri Oct 17 15:23:14 1997 +0200
    27.2 +++ b/src/HOL/Induct/SList.ML	Fri Oct 17 15:25:12 1997 +0200
    27.3 @@ -312,12 +312,12 @@
    27.4  
    27.5  goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
    27.6  by (list_ind_tac "xs" 1);
    27.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    27.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
    27.9  qed "mem_append2";
   27.10  
   27.11  goal SList.thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   27.12  by (list_ind_tac "xs" 1);
   27.13 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   27.14 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   27.15  qed "mem_filter2";
   27.16  
   27.17  
    28.1 --- a/src/HOL/Integ/Bin.ML	Fri Oct 17 15:23:14 1997 +0200
    28.2 +++ b/src/HOL/Integ/Bin.ML	Fri Oct 17 15:25:12 1997 +0200
    28.3 @@ -100,7 +100,7 @@
    28.4  
    28.5  (**** The carry/borrow functions, bin_succ and bin_pred ****)
    28.6  
    28.7 -val if_ss = !simpset setloop (split_tac [expand_if]) ;
    28.8 +val if_ss = !simpset addsplits [expand_if];
    28.9  
   28.10  
   28.11  (**** integ_of_bin ****)
    29.1 --- a/src/HOL/Lambda/Eta.ML	Fri Oct 17 15:23:14 1997 +0200
    29.2 +++ b/src/HOL/Lambda/Eta.ML	Fri Oct 17 15:25:12 1997 +0200
    29.3 @@ -37,8 +37,7 @@
    29.4  by (dB.induct_tac "t" 1);
    29.5  by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
    29.6  by (Blast_tac 2);
    29.7 -by(simp_tac (!simpset addsimps [pred_def]
    29.8 -                      setloop (split_tac [expand_nat_case])) 1);
    29.9 +by(simp_tac (!simpset addsimps [pred_def] addsplits [expand_nat_case]) 1);
   29.10  by (safe_tac HOL_cs);
   29.11  by (ALLGOALS trans_tac);
   29.12  qed "free_lift";
   29.13 @@ -51,7 +50,7 @@
   29.14  by (Blast_tac 2);
   29.15  by (asm_full_simp_tac (addsplit (!simpset)) 2);
   29.16  by(simp_tac (!simpset addsimps [pred_def,subst_Var]
   29.17 -                      setloop (split_tac [expand_if,expand_nat_case])) 1);
   29.18 +                      addsplits [expand_if,expand_nat_case]) 1);
   29.19  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   29.20  by (ALLGOALS trans_tac);
   29.21  qed "free_subst";
   29.22 @@ -169,7 +168,7 @@
   29.23  
   29.24  goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
   29.25  by (dB.induct_tac "s" 1);
   29.26 -  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   29.27 +  by (simp_tac (!simpset addsplits [expand_if]) 1);
   29.28    by (SELECT_GOAL(safe_tac HOL_cs)1);
   29.29     by(etac nat_neqE 1);
   29.30      by (res_inst_tac [("x","Var nat")] exI 1);
   29.31 @@ -180,7 +179,7 @@
   29.32     by (assume_tac 2);
   29.33    by (etac thin_rl 1);
   29.34    by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   29.35 -    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   29.36 +    by (simp_tac (!simpset addsplits [expand_if]) 1);
   29.37      by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
   29.38     by (Simp_tac 1);
   29.39    by (Simp_tac 1);
   29.40 @@ -196,7 +195,7 @@
   29.41   by (etac exE 1);
   29.42   by (etac rev_mp 1);
   29.43   by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   29.44 -   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   29.45 +   by (simp_tac (!simpset addsplits [expand_if]) 1);
   29.46    by (Simp_tac 1);
   29.47    by (Blast_tac 1);
   29.48   by (Simp_tac 1);
   29.49 @@ -210,7 +209,7 @@
   29.50  by (etac exE 1);
   29.51  by (etac rev_mp 1);
   29.52  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   29.53 -  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   29.54 +  by (simp_tac (!simpset addsplits [expand_if]) 1);
   29.55   by (Simp_tac 1);
   29.56  by (Simp_tac 1);
   29.57  by (Blast_tac 1);
    30.1 --- a/src/HOL/Lambda/Lambda.ML	Fri Oct 17 15:23:14 1997 +0200
    30.2 +++ b/src/HOL/Lambda/Lambda.ML	Fri Oct 17 15:25:12 1997 +0200
    30.3 @@ -45,8 +45,8 @@
    30.4  
    30.5  (*** subst and lift ***)
    30.6  
    30.7 -fun addsplit ss = ss addsimps [subst_Var] 
    30.8 -                     setloop  (split_inside_tac [expand_if]);
    30.9 +fun addsplit ss = ss addsimps [subst_Var]
   30.10 +                     setloop (split_inside_tac [expand_if]);
   30.11  
   30.12  goal Lambda.thy "(Var k)[u/k] = u";
   30.13  by (asm_full_simp_tac(addsplit(!simpset)) 1);
   30.14 @@ -66,7 +66,7 @@
   30.15  goal Lambda.thy
   30.16    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
   30.17  by (dB.induct_tac "t" 1);
   30.18 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])
   30.19 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if]
   30.20                                      addSolver cut_trans_tac)));
   30.21  by (safe_tac HOL_cs);
   30.22  by (ALLGOALS trans_tac);
   30.23 @@ -76,7 +76,7 @@
   30.24  \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
   30.25  by (dB.induct_tac "t" 1);
   30.26  by (ALLGOALS(asm_simp_tac (!simpset addsimps [pred_def,subst_Var,lift_lift]
   30.27 -                                setloop (split_tac [expand_if,expand_nat_case])
   30.28 +                                addsplits [expand_if,expand_nat_case]
   30.29                                  addSolver cut_trans_tac)));
   30.30  by (safe_tac HOL_cs);
   30.31  by (ALLGOALS trans_tac);
   30.32 @@ -88,7 +88,7 @@
   30.33  \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
   30.34  by (dB.induct_tac "t" 1);
   30.35  by (ALLGOALS(asm_simp_tac (!simpset addsimps [subst_Var,lift_lift]
   30.36 -                                setloop (split_tac [expand_if])
   30.37 +                                addsplits [expand_if]
   30.38                                  addSolver cut_trans_tac)));
   30.39  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   30.40  by (ALLGOALS trans_tac);
   30.41 @@ -96,7 +96,7 @@
   30.42  
   30.43  goal Lambda.thy "!k s. (lift t k)[s/k] = t";
   30.44  by (dB.induct_tac "t" 1);
   30.45 -by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac[expand_if]))));
   30.46 +by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if])));
   30.47  qed "subst_lift";
   30.48  Addsimps [subst_lift];
   30.49  
   30.50 @@ -106,7 +106,7 @@
   30.51  by (dB.induct_tac "t" 1);
   30.52  by (ALLGOALS(asm_simp_tac
   30.53        (!simpset addsimps [pred_def,subst_Var,lift_lift RS sym,lift_subst_lt]
   30.54 -                setloop (split_tac [expand_if,expand_nat_case])
   30.55 +                addsplits [expand_if,expand_nat_case]
   30.56                  addSolver cut_trans_tac)));
   30.57  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   30.58  by (ALLGOALS trans_tac);
    31.1 --- a/src/HOL/Lex/AutoChopper.ML	Fri Oct 17 15:23:14 1997 +0200
    31.2 +++ b/src/HOL/Lex/AutoChopper.ML	Fri Oct 17 15:25:12 1997 +0200
    31.3 @@ -18,7 +18,7 @@
    31.4  goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
    31.5  by (list.induct_tac "xs" 1);
    31.6  by (Simp_tac 1);
    31.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    31.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
    31.9  val accept_not_Nil = result() repeat_RS spec;
   31.10  Addsimps [accept_not_Nil];
   31.11  
   31.12 @@ -27,7 +27,7 @@
   31.13  \        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
   31.14  by (list.induct_tac "xs" 1);
   31.15  by (simp_tac (!simpset addcongs [conj_cong]) 1);
   31.16 -by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   31.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   31.18  by (strip_tac 1);
   31.19  by (rtac conjI 1);
   31.20  by (Fast_tac 1);
   31.21 @@ -53,17 +53,17 @@
   31.22  \    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
   31.23  \    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
   31.24  by (list.induct_tac "xs" 1);
   31.25 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   31.26 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   31.27 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
   31.28 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   31.29  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   31.30  by (rename_tac "vss lrst" 1);  
   31.31 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   31.32 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   31.33  by (res_inst_tac[("xs","vss")] list_eq_cases 1);
   31.34   by (hyp_subst_tac 1);
   31.35   by (Simp_tac 1);
   31.36   by (fast_tac (!claset addSDs [no_acc]) 1);
   31.37  by (hyp_subst_tac 1);
   31.38 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   31.39 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   31.40  val step2_a = (result() repeat_RS spec) RS mp;
   31.41  
   31.42  
   31.43 @@ -73,11 +73,11 @@
   31.44  \     (if acc_prefix A st xs \
   31.45  \      then ys ~= [] \
   31.46  \      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
   31.47 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   31.48 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   31.49  by (list.induct_tac "xs" 1);
   31.50 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   31.51 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
   31.52   by (Fast_tac 1);
   31.53 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   31.54 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
   31.55  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   31.56  by (rename_tac "vss lrst" 1);  
   31.57  by (Asm_simp_tac 1);
   31.58 @@ -96,11 +96,11 @@
   31.59  \     (if acc_prefix A st xs                   \
   31.60  \      then ? g. ys=r@g & fin A (nexts A st g)  \
   31.61  \      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
   31.62 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   31.63 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   31.64  by (list.induct_tac "xs" 1);
   31.65 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   31.66 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
   31.67   by (Fast_tac 1);
   31.68 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   31.69 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
   31.70  by (strip_tac 1);
   31.71  by (rtac conjI 1);
   31.72   by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   31.73 @@ -135,11 +135,11 @@
   31.74  \     (if acc_prefix A st xs       \
   31.75  \      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
   31.76  \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
   31.77 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   31.78 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   31.79  by (list.induct_tac "xs" 1);
   31.80 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   31.81 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
   31.82   by (Fast_tac 1);
   31.83 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
   31.84 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
   31.85  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   31.86  by (rename_tac "vss lrst" 1);  
   31.87  by (Asm_simp_tac 1);
   31.88 @@ -164,7 +164,7 @@
   31.89  by (Simp_tac 1);
   31.90  by (rtac trans 1);
   31.91   by (etac step2_a 1);
   31.92 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   31.93 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   31.94  val step2_d = (result() repeat_RS spec) RS mp;
   31.95  
   31.96  Delsimps [split_paired_All];
   31.97 @@ -174,11 +174,11 @@
   31.98  \  (if acc_prefix A st xs  \
   31.99  \   then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
  31.100  \   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
  31.101 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  31.102 +by (simp_tac (!simpset addsplits [expand_if]) 1);
  31.103  by (list.induct_tac "xs" 1);
  31.104 - by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
  31.105 + by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
  31.106   by (Fast_tac 1);
  31.107 -by (asm_simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
  31.108 +by (asm_simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
  31.109  by (strip_tac 1);
  31.110  by (case_tac "acc_prefix A (next A st a) list" 1);
  31.111   by (rtac conjI 1);
  31.112 @@ -225,18 +225,18 @@
  31.113  by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
  31.114   by (rtac mp 1);
  31.115    by (etac step2_b 2);
  31.116 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  31.117 + by (simp_tac (!simpset addsplits [expand_if]) 1);
  31.118  by (rtac conjI 1);
  31.119   by (rtac mp 1);
  31.120    by (etac step2_c 2);
  31.121 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  31.122 + by (simp_tac (!simpset addsplits [expand_if]) 1);
  31.123  by (rtac conjI 1);
  31.124 - by (asm_simp_tac (!simpset addsimps [step2_a] setloop (split_tac [expand_if])) 1);
  31.125 + by (asm_simp_tac (!simpset addsimps [step2_a] addsplits [expand_if]) 1);
  31.126  by (rtac conjI 1);
  31.127   by (rtac mp 1);
  31.128    by (etac step2_d 2);
  31.129 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  31.130 + by (simp_tac (!simpset addsplits [expand_if]) 1);
  31.131  by (rtac mp 1);
  31.132   by (etac step2_e 2);
  31.133 - by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  31.134 + by (simp_tac (!simpset addsplits [expand_if]) 1);
  31.135  qed"auto_chopper_is_auto_chopper";
    32.1 --- a/src/HOL/List.ML	Fri Oct 17 15:23:14 1997 +0200
    32.2 +++ b/src/HOL/List.ML	Fri Oct 17 15:25:12 1997 +0200
    32.3 @@ -203,17 +203,17 @@
    32.4  
    32.5  goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
    32.6  by (asm_simp_tac (!simpset addsimps [hd_append]
    32.7 -                           setloop (split_tac [expand_list_case])) 1);
    32.8 +                           addsplits [expand_list_case]) 1);
    32.9  qed "hd_append2";
   32.10  Addsimps [hd_append2];
   32.11  
   32.12  goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
   32.13 -by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
   32.14 +by (simp_tac (!simpset addsplits [expand_list_case]) 1);
   32.15  qed "tl_append";
   32.16  
   32.17  goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
   32.18  by (asm_simp_tac (!simpset addsimps [tl_append]
   32.19 -                           setloop (split_tac [expand_list_case])) 1);
   32.20 +                           addsplits [expand_list_case]) 1);
   32.21  qed "tl_append2";
   32.22  Addsimps [tl_append2];
   32.23  
   32.24 @@ -309,13 +309,13 @@
   32.25  
   32.26  goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
   32.27  by (induct_tac "xs" 1);
   32.28 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   32.29 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.30  qed "mem_append";
   32.31  Addsimps[mem_append];
   32.32  
   32.33  goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   32.34  by (induct_tac "xs" 1);
   32.35 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   32.36 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.37  qed "mem_filter";
   32.38  Addsimps[mem_filter];
   32.39  
   32.40 @@ -331,7 +331,7 @@
   32.41  
   32.42  goal thy "(x mem xs) = (x: set xs)";
   32.43  by (induct_tac "xs" 1);
   32.44 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   32.45 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.46  by (Blast_tac 1);
   32.47  qed "set_mem_eq";
   32.48  
   32.49 @@ -377,7 +377,7 @@
   32.50  
   32.51  goal thy "list_all P xs = (!x. x mem xs --> P(x))";
   32.52  by (induct_tac "xs" 1);
   32.53 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   32.54 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.55  by (Blast_tac 1);
   32.56  qed "list_all_mem_conv";
   32.57  
   32.58 @@ -388,13 +388,13 @@
   32.59  
   32.60  goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
   32.61  by (induct_tac "xs" 1);
   32.62 - by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   32.63 + by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.64  qed "filter_append";
   32.65  Addsimps [filter_append];
   32.66  
   32.67  goal thy "size (filter P xs) <= size xs";
   32.68  by (induct_tac "xs" 1);
   32.69 - by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   32.70 + by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.71  qed "filter_size";
   32.72  
   32.73  
   32.74 @@ -489,7 +489,7 @@
   32.75  (* case 0 *)
   32.76  by (Asm_full_simp_tac 1);
   32.77  (* case Suc x *)
   32.78 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   32.79 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   32.80  qed_spec_mp "nth_mem";
   32.81  Addsimps [nth_mem];
   32.82  
   32.83 @@ -497,36 +497,36 @@
   32.84  
   32.85  goal thy "last(xs@[x]) = x";
   32.86  by(induct_tac "xs" 1);
   32.87 -by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
   32.88 +by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.89  qed "last_snoc";
   32.90  Addsimps [last_snoc];
   32.91  
   32.92  goal thy "butlast(xs@[x]) = xs";
   32.93  by(induct_tac "xs" 1);
   32.94 -by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
   32.95 +by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   32.96  qed "butlast_snoc";
   32.97  Addsimps [butlast_snoc];
   32.98  
   32.99  goal thy
  32.100    "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
  32.101  by(induct_tac "xs" 1);
  32.102 -by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
  32.103 +by(ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
  32.104  qed_spec_mp "butlast_append";
  32.105  
  32.106  goal thy "x:set(butlast xs) --> x:set xs";
  32.107  by(induct_tac "xs" 1);
  32.108 -by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
  32.109 +by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
  32.110  qed_spec_mp "in_set_butlastD";
  32.111  
  32.112  goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
  32.113  by(asm_simp_tac (!simpset addsimps [butlast_append]
  32.114 -                          setloop (split_tac[expand_if])) 1);
  32.115 +                          addsplits [expand_if]) 1);
  32.116  by(blast_tac (!claset addDs [in_set_butlastD]) 1);
  32.117  qed "in_set_butlast_appendI1";
  32.118  
  32.119  goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
  32.120  by(asm_simp_tac (!simpset addsimps [butlast_append]
  32.121 -                          setloop (split_tac[expand_if])) 1);
  32.122 +                          addsplits [expand_if]) 1);
  32.123  by(Clarify_tac 1);
  32.124  by(Full_simp_tac 1);
  32.125  qed "in_set_butlast_appendI2";
  32.126 @@ -678,14 +678,14 @@
  32.127  goal thy "takeWhile P xs @ dropWhile P xs = xs";
  32.128  by (induct_tac "xs" 1);
  32.129   by (Simp_tac 1);
  32.130 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  32.131 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  32.132  qed "takeWhile_dropWhile_id";
  32.133  Addsimps [takeWhile_dropWhile_id];
  32.134  
  32.135  goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
  32.136  by (induct_tac "xs" 1);
  32.137   by (Simp_tac 1);
  32.138 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  32.139 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  32.140  by (Blast_tac 1);
  32.141  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
  32.142  Addsimps [takeWhile_append1];
  32.143 @@ -694,7 +694,7 @@
  32.144    "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
  32.145  by (induct_tac "xs" 1);
  32.146   by (Simp_tac 1);
  32.147 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  32.148 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  32.149  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
  32.150  Addsimps [takeWhile_append2];
  32.151  
  32.152 @@ -702,7 +702,7 @@
  32.153    "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
  32.154  by (induct_tac "xs" 1);
  32.155   by (Simp_tac 1);
  32.156 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  32.157 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  32.158  by (Blast_tac 1);
  32.159  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
  32.160  Addsimps [dropWhile_append1];
  32.161 @@ -711,14 +711,14 @@
  32.162    "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
  32.163  by (induct_tac "xs" 1);
  32.164   by (Simp_tac 1);
  32.165 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  32.166 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  32.167  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
  32.168  Addsimps [dropWhile_append2];
  32.169  
  32.170  goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
  32.171  by (induct_tac "xs" 1);
  32.172   by (Simp_tac 1);
  32.173 -by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  32.174 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  32.175  qed_spec_mp"set_take_whileD";
  32.176  
  32.177  (** replicate **)
    33.1 --- a/src/HOL/MiniML/Generalize.ML	Fri Oct 17 15:23:14 1997 +0200
    33.2 +++ b/src/HOL/MiniML/Generalize.ML	Fri Oct 17 15:25:12 1997 +0200
    33.3 @@ -45,8 +45,8 @@
    33.4  by (typ.induct_tac "t1" 1);
    33.5  by (Simp_tac 1);
    33.6  by (case_tac "nat : free_tv A" 1);
    33.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    33.8 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    33.9 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   33.10 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   33.11  by (Fast_tac 1);
   33.12  by (Asm_simp_tac 1);
   33.13  by (Fast_tac 1);
   33.14 @@ -99,7 +99,7 @@
   33.15  by (rename_tac "R" 1);
   33.16  by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
   33.17  by (typ.induct_tac "t" 1);
   33.18 - by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   33.19 + by (simp_tac (!simpset addsplits [expand_if]) 1);
   33.20  by (Asm_simp_tac 1);
   33.21  qed "gen_bound_typ_instance";
   33.22  
   33.23 @@ -109,7 +109,7 @@
   33.24  by (rename_tac "S" 1);
   33.25  by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
   33.26  by (typ.induct_tac "t" 1);
   33.27 - by (asm_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   33.28 + by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   33.29   by (Fast_tac 1);
   33.30  by (Asm_simp_tac 1);
   33.31  qed "free_tv_subset_gen_le";
   33.32 @@ -123,8 +123,8 @@
   33.33  by (typ.induct_tac "t" 1);
   33.34  by (Simp_tac 1);
   33.35  by (case_tac "nat : free_tv A" 1);
   33.36 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   33.37 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   33.38 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   33.39 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   33.40  by (subgoal_tac "n <= n + nat" 1);
   33.41  by (forw_inst_tac [("t","A")] new_tv_le 1);
   33.42  by (assume_tac 1);
    34.1 --- a/src/HOL/MiniML/Instance.ML	Fri Oct 17 15:23:14 1997 +0200
    34.2 +++ b/src/HOL/MiniML/Instance.ML	Fri Oct 17 15:25:12 1997 +0200
    34.3 @@ -66,8 +66,8 @@
    34.4  by (rename_tac "S1 S2" 1);
    34.5  by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
    34.6  by (safe_tac (!claset));
    34.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    34.8 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    34.9 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   34.10 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
   34.11  by (strip_tac 1);
   34.12  by (dres_inst_tac [("x","x")] bspec 1);
   34.13  by (assume_tac 1);
   34.14 @@ -82,8 +82,8 @@
   34.15  goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
   34.16  \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
   34.17  by (type_scheme.induct_tac "sch" 1);
   34.18 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
   34.19 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [le_add2,diff_add_inverse2]) 1);
   34.20 +by (simp_tac (!simpset addsimps [leD] addsplits [expand_if]) 1);
   34.21 +by (simp_tac (!simpset addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1);
   34.22  by (Asm_simp_tac 1);
   34.23  qed_spec_mp "subst_to_scheme_inverse";
   34.24  
   34.25 @@ -96,9 +96,9 @@
   34.26  \        (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
   34.27  \                         bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
   34.28  by (type_scheme.induct_tac "sch" 1);
   34.29 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
   34.30 +by (simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
   34.31  by (Asm_simp_tac 1);
   34.32 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [leD]) 1);
   34.33 +by (asm_full_simp_tac (!simpset addsplits [expand_if] addsimps [leD]) 1);
   34.34  val aux2 = result () RS mp;
   34.35  
   34.36  
    35.1 --- a/src/HOL/MiniML/Maybe.ML	Fri Oct 17 15:23:14 1997 +0200
    35.2 +++ b/src/HOL/MiniML/Maybe.ML	Fri Oct 17 15:25:12 1997 +0200
    35.3 @@ -25,7 +25,7 @@
    35.4  
    35.5  goal thy
    35.6    "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    35.7 -by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
    35.8 +by(simp_tac (!simpset addsplits [expand_option_bind]) 1);
    35.9  qed "option_bind_eq_None";
   35.10  
   35.11  Addsimps [option_bind_eq_None];
    36.1 --- a/src/HOL/MiniML/MiniML.ML	Fri Oct 17 15:23:14 1997 +0200
    36.2 +++ b/src/HOL/MiniML/MiniML.ML	Fri Oct 17 15:25:12 1997 +0200
    36.3 @@ -82,7 +82,7 @@
    36.4  goalw thy [free_tv_subst,dom_def]
    36.5            "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
    36.6  \               free_tv A Un free_tv t";
    36.7 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    36.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    36.9  by (Fast_tac 1);
   36.10  qed "dom_S'";
   36.11  
   36.12 @@ -110,7 +110,7 @@
   36.13  \         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
   36.14  \         {x. ? y. x = n + y}";
   36.15  by (typ.induct_tac "t1" 1);
   36.16 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   36.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   36.18  by (Fast_tac 1);
   36.19  by (Simp_tac 1);
   36.20  by (Fast_tac 1);
    37.1 --- a/src/HOL/MiniML/Type.ML	Fri Oct 17 15:23:14 1997 +0200
    37.2 +++ b/src/HOL/MiniML/Type.ML	Fri Oct 17 15:25:12 1997 +0200
    37.3 @@ -352,7 +352,7 @@
    37.4  
    37.5  goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
    37.6  by (type_scheme.induct_tac "sch" 1);
    37.7 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    37.8 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    37.9  by (strip_tac 1);
   37.10  by (Fast_tac 1);
   37.11  qed "free_tv_ML_scheme";
   37.12 @@ -423,14 +423,14 @@
   37.13  goal thy
   37.14    "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
   37.15  by (typ.induct_tac "t" 1);
   37.16 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   37.17 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   37.18  qed "subst_te_new_tv";
   37.19  Addsimps [subst_te_new_tv];
   37.20  
   37.21  goal thy
   37.22    "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
   37.23  by (type_scheme.induct_tac "sch" 1);
   37.24 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   37.25 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   37.26  qed_spec_mp "subst_te_new_type_scheme";
   37.27  Addsimps [subst_te_new_type_scheme];
   37.28  
   37.29 @@ -546,13 +546,13 @@
   37.30  Addsimps [new_tv_not_free_tv];
   37.31  
   37.32  goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
   37.33 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   37.34 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   37.35  by (safe_tac (!claset));
   37.36  by (trans_tac 1);
   37.37  qed "less_maxL";
   37.38  
   37.39  goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
   37.40 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   37.41 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   37.42  by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1);
   37.43  val less_maxR = result();
   37.44  
   37.45 @@ -585,11 +585,11 @@
   37.46  Addsimps [fresh_variable_type_schemes];
   37.47  
   37.48  goalw thy [max_def] "!!n::nat. n <= (max n n')";
   37.49 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   37.50 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   37.51  val le_maxL = result();
   37.52  
   37.53  goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
   37.54 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   37.55 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   37.56  by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
   37.57  val le_maxR = result();
   37.58  
    38.1 --- a/src/HOL/MiniML/W.ML	Fri Oct 17 15:23:14 1997 +0200
    38.2 +++ b/src/HOL/MiniML/W.ML	Fri Oct 17 15:25:12 1997 +0200
    38.3 @@ -18,7 +18,7 @@
    38.4          "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
    38.5  by (expr.induct_tac "e" 1);
    38.6  (* case Var(n) *)
    38.7 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
    38.8 +by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
    38.9  by (strip_tac 1);
   38.10  by (etac conjE 1);
   38.11  by (etac conjE 1);
   38.12 @@ -27,10 +27,10 @@
   38.13  by (dtac sym 1);
   38.14  by (Asm_full_simp_tac 1);
   38.15  (* case Abs e *)
   38.16 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
   38.17 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
   38.18  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   38.19  (* case App e1 e2 *)
   38.20 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
   38.21 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
   38.22  by (strip_tac 1);
   38.23  by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
   38.24  by (eres_inst_tac [("x","A")] allE 1);
   38.25 @@ -50,7 +50,7 @@
   38.26  by (Asm_simp_tac 1);
   38.27  by (Asm_simp_tac 1);
   38.28  (* case LET e1 e2 *)
   38.29 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
   38.30 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
   38.31  by (strip_tac 1);
   38.32  by (rename_tac "A n1 S t2 m1 S2 t3 m2 S3 t1 m" 1);
   38.33  by (REPEAT (etac conjE 1));
   38.34 @@ -88,7 +88,7 @@
   38.35  by (assume_tac 2);
   38.36  by (rtac add_le_mono 1);
   38.37  by (Simp_tac 1);
   38.38 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
   38.39 +by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
   38.40  by (strip_tac 1);
   38.41  by (rtac new_tv_le 1);
   38.42  by (mp_tac 2);
   38.43 @@ -96,7 +96,7 @@
   38.44  by (assume_tac 2);
   38.45  by (rtac add_le_mono 1);
   38.46  by (Simp_tac 1);
   38.47 -by (simp_tac (!simpset setloop (split_tac [expand_if]) addsimps [max_def]) 1);
   38.48 +by (simp_tac (!simpset addsplits [expand_if] addsimps [max_def]) 1);
   38.49  by (strip_tac 1);
   38.50  by (dtac not_leE 1);
   38.51  by (rtac less_or_eq_imp_le 1);
   38.52 @@ -111,7 +111,7 @@
   38.53  \                 new_tv m S & new_tv m t";
   38.54  by (expr.induct_tac "e" 1);
   38.55  (* case Var n *)
   38.56 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind,expand_if])) 1);
   38.57 +by (simp_tac (!simpset addsplits [expand_option_bind,expand_if]) 1);
   38.58  by (strip_tac 1);
   38.59  by (REPEAT (etac conjE 1));
   38.60  by (rtac conjI 1);
   38.61 @@ -125,14 +125,14 @@
   38.62  by (Asm_full_simp_tac 1);
   38.63  (* case Abs e *)
   38.64  by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
   38.65 -    setloop (split_tac [expand_option_bind])) 1);
   38.66 +    addsplits [expand_option_bind]) 1);
   38.67  by (strip_tac 1);
   38.68  by (eres_inst_tac [("x","Suc n")] allE 1);
   38.69  by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
   38.70  by (fast_tac (HOL_cs addss (!simpset
   38.71                addsimps [new_tv_subst,new_tv_Suc_list])) 1);
   38.72  (* case App e1 e2 *)
   38.73 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
   38.74 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
   38.75  by (strip_tac 1);
   38.76  by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m" 1);
   38.77  by (eres_inst_tac [("x","n")] allE 1);
   38.78 @@ -174,7 +174,7 @@
   38.79       [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_le]
   38.80       addss (!simpset)) 1);
   38.81  (* case LET e1 e2 *)
   38.82 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
   38.83 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
   38.84  by (strip_tac 1);
   38.85  by (rename_tac "n1 A S1 t1 n2 S2 t2 m2 S t m" 1);
   38.86  by (REPEAT (etac conjE 1));
   38.87 @@ -239,7 +239,7 @@
   38.88  by (expr.induct_tac "e" 1);
   38.89  (* case Var n *)
   38.90  by (simp_tac (!simpset addsimps
   38.91 -    [free_tv_subst] setloop (split_tac [expand_option_bind,expand_if])) 1);
   38.92 +    [free_tv_subst] addsplits [expand_option_bind,expand_if]) 1);
   38.93  by (strip_tac 1);
   38.94  by (REPEAT (etac conjE 1));
   38.95  by (hyp_subst_tac 1);
   38.96 @@ -255,7 +255,7 @@
   38.97  by (Asm_full_simp_tac 1);
   38.98  (* case Abs e *)
   38.99  by (asm_full_simp_tac (!simpset addsimps
  38.100 -    [free_tv_subst] setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
  38.101 +    [free_tv_subst] addsplits [expand_option_bind] delsimps all_simps) 1);
  38.102  by (strip_tac 1);
  38.103  by (rename_tac "S t n1 S1 t1 m v" 1);
  38.104  by (eres_inst_tac [("x","Suc n")] allE 1);
  38.105 @@ -267,7 +267,7 @@
  38.106  by (best_tac (HOL_cs addIs [cod_app_subst]
  38.107                       addss (!simpset addsimps [less_Suc_eq])) 1);
  38.108  (* case App e1 e2 *)
  38.109 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
  38.110 +by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
  38.111  by (strip_tac 1); 
  38.112  by (rename_tac "S t n1 S1 t1 n2 S2 S3 t2 m v" 1);
  38.113  by (eres_inst_tac [("x","n")] allE 1);
  38.114 @@ -303,7 +303,7 @@
  38.115    addEs [UnE]
  38.116    addss !simpset) 1);
  38.117  (* LET e1 e2 *)
  38.118 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind]) delsimps all_simps) 1);
  38.119 +by (simp_tac (!simpset addsplits [expand_option_bind] delsimps all_simps) 1);
  38.120  by (strip_tac 1); 
  38.121  by (rename_tac "nat A S1 t1 n2 S2 t2 m2 S t m v" 1);
  38.122  by (eres_inst_tac [("x","nat")] allE 1);
  38.123 @@ -338,7 +338,7 @@
  38.124          "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
  38.125  by (expr.induct_tac "e" 1);
  38.126  (* case Var n *)
  38.127 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  38.128 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  38.129  by (strip_tac 1);
  38.130  by (rtac has_type.VarI 1);
  38.131  by (Simp_tac 1);
  38.132 @@ -347,7 +347,7 @@
  38.133  by (rtac refl 1);
  38.134  (* case Abs e *)
  38.135  by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
  38.136 -                        setloop (split_tac [expand_option_bind])) 1);
  38.137 +                        addsplits [expand_option_bind]) 1);
  38.138  by (strip_tac 1);
  38.139  by (eres_inst_tac [("x","(mk_scheme (TVar n)) # A")] allE 1);
  38.140  by (Asm_full_simp_tac 1);
  38.141 @@ -360,7 +360,7 @@
  38.142  by (Asm_simp_tac 1);
  38.143  by (assume_tac 1);
  38.144  (* case App e1 e2 *)
  38.145 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
  38.146 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
  38.147  by (strip_tac 1);
  38.148  by (rename_tac "S1 t1 n1 S2 t2 n2 S3" 1);
  38.149  by (res_inst_tac [("t2.0","$ S3 t2")] has_type.AppI 1);
  38.150 @@ -392,7 +392,7 @@
  38.151  by (mp_tac 1);
  38.152  by (assume_tac 1);
  38.153  (* case Let e1 e2 *)
  38.154 -by (simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
  38.155 +by (simp_tac (!simpset addsplits [expand_option_bind]) 1);
  38.156  by (strip_tac 1);
  38.157  by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); 
  38.158  by (res_inst_tac [("t1.0","$ S2 t1")] has_type.LETI 1);
  38.159 @@ -469,8 +469,7 @@
  38.160  by (expr.induct_tac "e" 1);
  38.161  (* case Var n *)
  38.162  by (strip_tac 1);
  38.163 -by (simp_tac (!simpset addcongs [conj_cong] 
  38.164 -    setloop (split_tac [expand_if])) 1);
  38.165 +by (simp_tac (!simpset addcongs [conj_cong] addsplits [expand_if]) 1);
  38.166  by (eresolve_tac has_type_casesE 1); 
  38.167  by (asm_full_simp_tac (!simpset addsimps [is_bound_typ_instance]) 1);
  38.168  by (etac exE 1);
  38.169 @@ -491,7 +490,7 @@
  38.170  by (eres_inst_tac [("x","Suc n")] allE 1);
  38.171  by (best_tac (HOL_cs addSDs [mk_scheme_injective] 
  38.172                    addss (!simpset addcongs [conj_cong] 
  38.173 -                                setloop (split_tac [expand_option_bind]))) 1);
  38.174 +                                addsplits [expand_option_bind])) 1);
  38.175  (** LEVEL 19 **)
  38.176  
  38.177  (* case App e1 e2 *)
  38.178 @@ -531,8 +530,7 @@
  38.179  by (case_tac "na:free_tv Sa" 2);
  38.180  (* n1 ~: free_tv S1 *)
  38.181  by (forward_tac [not_free_impl_id] 3);
  38.182 -by (asm_simp_tac (!simpset 
  38.183 -    setloop (split_tac [expand_if])) 3);
  38.184 +by (asm_simp_tac (!simpset addsplits [expand_if]) 3);
  38.185  (* na : free_tv Sa *)
  38.186  by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
  38.187  by (dtac eq_subst_scheme_list_eq_free 2);
  38.188 @@ -540,8 +538,7 @@
  38.189  by (Asm_simp_tac 2); 
  38.190  by (case_tac "na:dom Sa" 2);
  38.191  (* na ~: dom Sa *)
  38.192 -by (asm_full_simp_tac (!simpset addsimps [dom_def] 
  38.193 -    setloop (split_tac [expand_if])) 3);
  38.194 +by (asm_full_simp_tac (!simpset addsimps [dom_def] addsplits [expand_if]) 3);
  38.195  (* na : dom Sa *)
  38.196  by (rtac eq_free_eq_subst_te 2);
  38.197  by (strip_tac 2);
  38.198 @@ -553,7 +550,7 @@
  38.199  by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
  38.200      (!simpset addsimps [cod_def,free_tv_subst])) 3);
  38.201  by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
  38.202 -    setloop (split_tac [expand_if]))) 2);
  38.203 +                                     addsplits [expand_if])) 2);
  38.204  by (Simp_tac 2);  
  38.205  by (rtac eq_free_eq_subst_te 2);
  38.206  by (strip_tac 2 );
  38.207 @@ -564,16 +561,16 @@
  38.208  by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
  38.209  by (case_tac "na: free_tv t - free_tv Sa" 2);
  38.210  (* case na ~: free_tv t - free_tv Sa *)
  38.211 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
  38.212 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
  38.213  by (Fast_tac 3);
  38.214  (* case na : free_tv t - free_tv Sa *)
  38.215 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
  38.216 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
  38.217  by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
  38.218  by (dtac eq_subst_scheme_list_eq_free 2);
  38.219  by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
  38.220  (** LEVEL 75 **)
  38.221  by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
  38.222 -by (asm_simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); 
  38.223 +by (asm_simp_tac (!simpset addsplits [expand_option_bind]) 1); 
  38.224  by (safe_tac HOL_cs );
  38.225  by (dtac mgu_Some 1);
  38.226  by ( fast_tac (HOL_cs addss !simpset) 1);
  38.227 @@ -603,9 +600,9 @@
  38.228      new_tv_not_free_tv]) 2);
  38.229  by (case_tac "na: free_tv t - free_tv Sa" 1);
  38.230  (* case na ~: free_tv t - free_tv Sa *)
  38.231 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
  38.232 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
  38.233  (* case na : free_tv t - free_tv Sa *)
  38.234 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  38.235 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  38.236  by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
  38.237  by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
  38.238      eq_subst_scheme_list_eq_free] addss ((!simpset addsimps 
    39.1 --- a/src/HOL/Prod.ML	Fri Oct 17 15:23:14 1997 +0200
    39.2 +++ b/src/HOL/Prod.ML	Fri Oct 17 15:25:12 1997 +0200
    39.3 @@ -168,7 +168,7 @@
    39.4  qed "expand_split";
    39.5  
    39.6  (* could be done after split_tac has been speeded up significantly:
    39.7 -simpset := (!simpset setloop split_tac[expand_split]);
    39.8 +simpset := (!simpset addsplits [expand_split]);
    39.9     precompute the constants involved and don't do anything unless
   39.10     the current goal contains one of those constants
   39.11  *)
    40.1 --- a/src/HOL/Set.ML	Fri Oct 17 15:23:14 1997 +0200
    40.2 +++ b/src/HOL/Set.ML	Fri Oct 17 15:25:12 1997 +0200
    40.3 @@ -646,7 +646,7 @@
    40.4  
    40.5  
    40.6  (** Rewrite rules for boolean case-splitting: faster than 
    40.7 -	setloop split_tac[expand_if]
    40.8 +	addsplits[expand_if]
    40.9  **)
   40.10  
   40.11  bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
   40.12 @@ -669,7 +669,7 @@
   40.13  
   40.14  (*Not for Addsimps -- it can cause goals to blow up!*)
   40.15  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
   40.16 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   40.17 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   40.18  qed "mem_if";
   40.19  
   40.20  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    41.1 --- a/src/HOL/Subst/Subst.ML	Fri Oct 17 15:23:14 1997 +0200
    41.2 +++ b/src/HOL/Subst/Subst.ML	Fri Oct 17 15:25:12 1997 +0200
    41.3 @@ -41,8 +41,7 @@
    41.4  qed "agreement";
    41.5  
    41.6  goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
    41.7 -by (simp_tac (!simpset addsimps [agreement]
    41.8 -                      setloop (split_tac [expand_if])) 1);
    41.9 +by (simp_tac (!simpset addsimps [agreement] addsplits [expand_if]) 1);
   41.10  qed_spec_mp"repl_invariance";
   41.11  
   41.12  val asms = goal Subst.thy 
   41.13 @@ -112,7 +111,7 @@
   41.14  by (induct_tac "t" 1);
   41.15  by (ALLGOALS Asm_simp_tac);
   41.16  by (alist_ind_tac "r" 1);
   41.17 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   41.18 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   41.19  qed "subst_comp";
   41.20  
   41.21  Addsimps [subst_comp];
   41.22 @@ -131,7 +130,7 @@
   41.23  by (simp_tac (!simpset addsimps [subst_eq_iff]) 1);
   41.24  by (rtac allI 1);
   41.25  by (induct_tac "t" 1);
   41.26 -by (ALLGOALS (asm_full_simp_tac (!simpset setloop (split_tac [expand_if]))));
   41.27 +by (ALLGOALS (asm_full_simp_tac (!simpset addsplits [expand_if])));
   41.28  qed "Cons_trivial";
   41.29  
   41.30  
   41.31 @@ -144,7 +143,7 @@
   41.32  
   41.33  goal Subst.thy  "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
   41.34  by (alist_ind_tac "s" 1);
   41.35 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
   41.36 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   41.37  by (Blast_tac 1);
   41.38  qed "sdom_iff";
   41.39  
   41.40 @@ -204,7 +203,7 @@
   41.41  
   41.42  goal Subst.thy "(M <| [(x, Var x)]) = M";
   41.43  by (induct_tac "M" 1);
   41.44 -by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   41.45 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   41.46  qed "id_subst_lemma";
   41.47  
   41.48  Addsimps [id_subst_lemma];
    42.1 --- a/src/HOL/Subst/Unifier.ML	Fri Oct 17 15:23:14 1997 +0200
    42.2 +++ b/src/HOL/Subst/Unifier.ML	Fri Oct 17 15:25:12 1997 +0200
    42.3 @@ -83,7 +83,7 @@
    42.4  goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
    42.5  by (simp_tac (!simpset addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
    42.6  				 empty_iff_all_not]
    42.7 -                       setloop (split_tac [expand_if])) 1);
    42.8 +                       addsplits [expand_if]) 1);
    42.9  by (Blast_tac 1);
   42.10  qed_spec_mp "Var_Idem";
   42.11  
    43.1 --- a/src/HOL/Subst/Unify.ML	Fri Oct 17 15:23:14 1997 +0200
    43.2 +++ b/src/HOL/Subst/Unify.ML	Fri Oct 17 15:25:12 1997 +0200
    43.3 @@ -154,14 +154,14 @@
    43.4  by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
    43.5  by (ALLGOALS 
    43.6      (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
    43.7 -			    setloop (split_tac [expand_if]))));
    43.8 +			    addsplits [expand_if])));
    43.9  (*Const-Const case*)
   43.10  by (simp_tac
   43.11      (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
   43.12  			inv_image_def, less_eq]) 1);
   43.13  (** LEVEL 7 **)
   43.14  (*Comb-Comb case*)
   43.15 -by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
   43.16 +by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
   43.17  by (strip_tac 1);
   43.18  by (rtac (trans_unifyRel RS transD) 1);
   43.19  by (Blast_tac 1);
   43.20 @@ -184,7 +184,7 @@
   43.21  \                            of None => None    \
   43.22  \                             | Some sigma => Some (theta <> sigma)))";
   43.23  by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
   43.24 -			   setloop split_tac [expand_option_case]) 1);
   43.25 +			   addsplits [expand_option_case]) 1);
   43.26  qed "unifyCombComb";
   43.27  
   43.28  
   43.29 @@ -207,7 +207,7 @@
   43.30  
   43.31  goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
   43.32  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
   43.33 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   43.34 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   43.35  (*Const-Const case*)
   43.36  by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
   43.37  (*Const-Var case*)
   43.38 @@ -220,7 +220,7 @@
   43.39  by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
   43.40  (** LEVEL 8 **)
   43.41  (*Comb-Comb case*)
   43.42 -by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
   43.43 +by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
   43.44  by (strip_tac 1);
   43.45  by (rotate_tac ~2 1);
   43.46  by (asm_full_simp_tac 
   43.47 @@ -246,7 +246,7 @@
   43.48  by (ALLGOALS 
   43.49      (asm_simp_tac 
   43.50         (!simpset addsimps [Var_Idem] 
   43.51 -	         setloop split_tac[expand_if, expand_option_case])));
   43.52 +	         addsplits [expand_if,expand_option_case])));
   43.53  (*Comb-Comb case*)
   43.54  by (safe_tac (!claset));
   43.55  by (REPEAT (dtac spec 1 THEN mp_tac 1));
    44.1 --- a/src/HOL/W0/I.ML	Fri Oct 17 15:23:14 1997 +0200
    44.2 +++ b/src/HOL/W0/I.ML	Fri Oct 17 15:25:12 1997 +0200
    44.3 @@ -144,8 +144,7 @@
    44.4  goal I.thy "!a m s. \
    44.5  \  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
    44.6  by (expr.induct_tac "e" 1);
    44.7 -  by (simp_tac (!simpset addsimps [app_subst_list]
    44.8 -                        setloop (split_tac [expand_if])) 1);
    44.9 +  by (simp_tac (!simpset addsimps [app_subst_list] addsplits [expand_if]) 1);
   44.10   by (Simp_tac 1);
   44.11   by (strip_tac 1);
   44.12   by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
    45.1 --- a/src/HOL/W0/Maybe.ML	Fri Oct 17 15:23:14 1997 +0200
    45.2 +++ b/src/HOL/W0/Maybe.ML	Fri Oct 17 15:25:12 1997 +0200
    45.3 @@ -26,7 +26,7 @@
    45.4  
    45.5  goal Maybe.thy
    45.6    "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
    45.7 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
    45.8 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
    45.9  qed "bind_eq_Fail";
   45.10  
   45.11  Addsimps [bind_eq_Fail];
    46.1 --- a/src/HOL/W0/Type.ML	Fri Oct 17 15:23:14 1997 +0200
    46.2 +++ b/src/HOL/W0/Type.ML	Fri Oct 17 15:25:12 1997 +0200
    46.3 @@ -157,7 +157,7 @@
    46.4  goal thy
    46.5    "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
    46.6  by (typ.induct_tac "t" 1);
    46.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    46.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
    46.9  qed "subst_te_new_tv";
   46.10  Addsimps [subst_te_new_tv];
   46.11  
   46.12 @@ -259,7 +259,7 @@
   46.13  (* case [] *)
   46.14  by (Simp_tac 1);
   46.15  (* case x#xl *)
   46.16 -by (fast_tac (set_cs addss(!simpset setloop (split_tac [expand_if]))) 1);
   46.17 +by (fast_tac (set_cs addss(!simpset addsplits [expand_if])) 1);
   46.18  qed_spec_mp "ftv_mem_sub_ftv_list";
   46.19  Addsimps [ftv_mem_sub_ftv_list];
   46.20  
    47.1 --- a/src/HOL/W0/W.ML	Fri Oct 17 15:23:14 1997 +0200
    47.2 +++ b/src/HOL/W0/W.ML	Fri Oct 17 15:25:12 1997 +0200
    47.3 @@ -14,15 +14,15 @@
    47.4          "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
    47.5  by (expr.induct_tac "e" 1);
    47.6  (* case Var n *)
    47.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    47.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
    47.9  (* case Abs e *)
   47.10  by (asm_full_simp_tac (!simpset addsimps [app_subst_list]
   47.11 -                        setloop (split_tac [expand_bind])) 1);
   47.12 +                        addsplits [expand_bind]) 1);
   47.13  by (strip_tac 1);
   47.14  by (dtac sym 1);
   47.15  by (fast_tac (HOL_cs addss !simpset) 1);
   47.16  (* case App e1 e2 *)
   47.17 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   47.18 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
   47.19  by (strip_tac 1);
   47.20  by ( rename_tac "sa ta na sb tb nb sc" 1);
   47.21  by (res_inst_tac [("t2.0","$ sc tb")] has_type.AppI 1);
   47.22 @@ -45,12 +45,12 @@
   47.23          "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
   47.24  by (expr.induct_tac "e" 1);
   47.25  (* case Var(n) *)
   47.26 -by (fast_tac (HOL_cs addss(!simpset setloop (split_tac [expand_if]))) 1);
   47.27 +by (fast_tac (HOL_cs addss(!simpset addsplits [expand_if])) 1);
   47.28  (* case Abs e *)
   47.29 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   47.30 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
   47.31  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   47.32  (* case App e1 e2 *)
   47.33 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   47.34 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
   47.35  by (strip_tac 1);
   47.36  by (rename_tac "s t na sa ta nb sb sc tb m" 1);
   47.37  by (eres_inst_tac [("x","a")] allE 1);
   47.38 @@ -93,10 +93,10 @@
   47.39  (* case Var n *)
   47.40  by (fast_tac (HOL_cs addDs [list_all_nth] addss (!simpset 
   47.41          addsimps [id_subst_def,new_tv_list,new_tv_subst] 
   47.42 -        setloop (split_tac [expand_if]))) 1);
   47.43 +        addsplits [expand_if])) 1);
   47.44  (* case Abs e *)
   47.45  by (simp_tac (!simpset addsimps [new_tv_subst,new_tv_Suc_list] 
   47.46 -    setloop (split_tac [expand_bind])) 1);
   47.47 +    addsplits [expand_bind]) 1);
   47.48  by (strip_tac 1);
   47.49  by (eres_inst_tac [("x","Suc n")] allE 1);
   47.50  by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
   47.51 @@ -104,7 +104,7 @@
   47.52                addsimps [new_tv_subst,new_tv_Suc_list])) 1);
   47.53  
   47.54  (* case App e1 e2 *)
   47.55 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   47.56 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
   47.57  by (strip_tac 1);
   47.58  by (rename_tac "s t na sa ta nb sb sc tb m" 1);
   47.59  by (eres_inst_tac [("x","n")] allE 1);
   47.60 @@ -160,11 +160,11 @@
   47.61  by (expr.induct_tac "e" 1);
   47.62  (* case Var n *)
   47.63  by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
   47.64 -    addss (!simpset setloop (split_tac [expand_if]))) 1);
   47.65 +    addss (!simpset addsplits [expand_if])) 1);
   47.66  
   47.67  (* case Abs e *)
   47.68  by (asm_full_simp_tac (!simpset addsimps
   47.69 -    [free_tv_subst] setloop (split_tac [expand_bind])) 1);
   47.70 +    [free_tv_subst] addsplits [expand_bind]) 1);
   47.71  by (strip_tac 1);
   47.72  by (rename_tac "s t na sa ta m v" 1);
   47.73  by (eres_inst_tac [("x","Suc n")] allE 1);
   47.74 @@ -178,7 +178,7 @@
   47.75                       addss (!simpset addsimps [less_Suc_eq])) 1);
   47.76  (** LEVEL 12 **)
   47.77  (* case App e1 e2 *)
   47.78 -by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
   47.79 +by (simp_tac (!simpset addsplits [expand_bind]) 1);
   47.80  by (strip_tac 1); 
   47.81  by (rename_tac "s t na sa ta nb sb sc tb m v" 1);
   47.82  by (eres_inst_tac [("x","n")] allE 1);
   47.83 @@ -227,7 +227,7 @@
   47.84  (* case Var n *)
   47.85  by (strip_tac 1);
   47.86  by (simp_tac (!simpset addcongs [conj_cong] 
   47.87 -              setloop (split_tac [expand_if])) 1);
   47.88 +              addsplits [expand_if]) 1);
   47.89  by (eresolve_tac has_type_casesE 1); 
   47.90  by (asm_full_simp_tac (!simpset addsimps [eq_sym_conv,app_subst_list]) 1);
   47.91  by (res_inst_tac [("x","s'")] exI 1);
   47.92 @@ -242,7 +242,7 @@
   47.93  by (eres_inst_tac [("x","t2")] allE 1);
   47.94  by (eres_inst_tac [("x","Suc n")] allE 1);
   47.95  by (fast_tac (HOL_cs addss (!simpset addcongs [conj_cong]
   47.96 -                            setloop (split_tac [expand_bind]))) 1);
   47.97 +                            addsplits [expand_bind])) 1);
   47.98  
   47.99  (** LEVEL 17 **)
  47.100  (* case App e1 e2 *)
  47.101 @@ -285,7 +285,7 @@
  47.102  by (case_tac "na:free_tv sa" 2);
  47.103  (* na ~: free_tv sa *)
  47.104  by (forward_tac [not_free_impl_id] 3);
  47.105 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
  47.106 +by (asm_simp_tac (!simpset addsplits [expand_if]) 3);
  47.107  (* na : free_tv sa *)
  47.108  by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
  47.109  by (dtac eq_subst_tel_eq_free 2);
  47.110 @@ -295,7 +295,7 @@
  47.111  (* na ~: dom sa *)
  47.112  (** LEVEL 50 **)
  47.113  by (asm_full_simp_tac (!simpset addsimps [dom_def] 
  47.114 -                       setloop (split_tac [expand_if])) 3);
  47.115 +                       addsplits [expand_if]) 3);
  47.116  (* na : dom sa *)
  47.117  by (rtac eq_free_eq_subst_te 2);
  47.118  by (strip_tac 2);
  47.119 @@ -307,7 +307,7 @@
  47.120  by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
  47.121                (!simpset addsimps [cod_def,free_tv_subst])) 3);
  47.122  by (fast_tac (set_cs addss (!simpset addsimps [cod_def,free_tv_subst] 
  47.123 -                            setloop (split_tac [expand_if]))) 2);
  47.124 +                            addsplits [expand_if])) 2);
  47.125  
  47.126  (** LEVEL 60 **)
  47.127  by (Simp_tac 2);  
  47.128 @@ -321,16 +321,16 @@
  47.129  by (case_tac "na: free_tv t - free_tv sa" 2);
  47.130  (** LEVEL 69 **)
  47.131  (* case na ~: free_tv t - free_tv sa *)
  47.132 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 3);
  47.133 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 3);
  47.134  (* case na : free_tv t - free_tv sa *)
  47.135 -by ( asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
  47.136 +by ( asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
  47.137  by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
  47.138  by (dtac eq_subst_tel_eq_free 2);
  47.139  by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
  47.140  by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def]) 2);
  47.141  by (Fast_tac 2);
  47.142  (** LEVEL 76 **)
  47.143 -by (asm_simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
  47.144 +by (asm_simp_tac (!simpset addsplits [expand_bind]) 1);
  47.145  by (safe_tac HOL_cs);
  47.146  by (dtac mgu_Ok 1);
  47.147  by ( fast_tac (HOL_cs addss !simpset) 1);
  47.148 @@ -359,9 +359,9 @@
  47.149      new_tv_not_free_tv]) 2);
  47.150  by (case_tac "na: free_tv t - free_tv sa" 1);
  47.151  (* case na ~: free_tv t - free_tv sa *)
  47.152 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 2);
  47.153 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 2);
  47.154  (* case na : free_tv t - free_tv sa *)
  47.155 -by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  47.156 +by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
  47.157  by (dtac (free_tv_app_subst_tel RS subsetD) 1);
  47.158  by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
  47.159                              eq_subst_tel_eq_free] 
    48.1 --- a/src/HOL/WF.ML	Fri Oct 17 15:23:14 1997 +0200
    48.2 +++ b/src/HOL/WF.ML	Fri Oct 17 15:25:12 1997 +0200
    48.3 @@ -151,8 +151,7 @@
    48.4    H_cong to expose the equality*)
    48.5  goalw WF.thy [cut_def]
    48.6      "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
    48.7 -by (simp_tac (HOL_ss addsimps [expand_fun_eq]
    48.8 -                    setloop (split_tac [expand_if])) 1);
    48.9 +by (simp_tac (HOL_ss addsimps [expand_fun_eq] addsplits [expand_if]) 1);
   48.10  qed "cuts_eq";
   48.11  
   48.12  goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
   48.13 @@ -193,7 +192,7 @@
   48.14  by (cut_facts_tac prems 1);
   48.15  by (rtac ext 1);
   48.16  by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
   48.17 -                              setloop (split_tac [expand_if])) 1);
   48.18 +                              addsplits [expand_if]) 1);
   48.19  qed "is_recfun_cut";
   48.20  
   48.21  (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
    49.1 --- a/src/HOL/equalities.ML	Fri Oct 17 15:23:14 1997 +0200
    49.2 +++ b/src/HOL/equalities.ML	Fri Oct 17 15:25:12 1997 +0200
    49.3 @@ -239,13 +239,13 @@
    49.4  
    49.5  goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
    49.6  \                                          else        B Int C)";
    49.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    49.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    49.9  by (Blast_tac 1);
   49.10  qed "Int_insert_left";
   49.11  
   49.12  goal Set.thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
   49.13  \                                          else        A Int B)";
   49.14 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   49.15 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   49.16  by (Blast_tac 1);
   49.17  qed "Int_insert_right";
   49.18  
   49.19 @@ -568,7 +568,7 @@
   49.20  qed "Diff_insert2";
   49.21  
   49.22  goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
   49.23 -by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
   49.24 +by (simp_tac (!simpset addsplits [expand_if]) 1);
   49.25  by (Blast_tac 1);
   49.26  qed "insert_Diff_if";
   49.27  
    50.1 --- a/src/HOL/ex/Fib.ML	Fri Oct 17 15:23:14 1997 +0200
    50.2 +++ b/src/HOL/ex/Fib.ML	Fri Oct 17 15:25:12 1997 +0200
    50.3 @@ -53,7 +53,7 @@
    50.4  by (ALLGOALS  (*using fib.rules here results in a longer proof!*)
    50.5      (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, 
    50.6  				      mod_less, mod_Suc]
    50.7 -                            setloop split_tac[expand_if])));
    50.8 +                            addsplits [expand_if])));
    50.9  by (safe_tac (!claset addSDs [mod2_neq_0]));
   50.10  by (ALLGOALS
   50.11      (asm_full_simp_tac
    51.1 --- a/src/HOL/ex/InSort.ML	Fri Oct 17 15:23:14 1997 +0200
    51.2 +++ b/src/HOL/ex/InSort.ML	Fri Oct 17 15:25:12 1997 +0200
    51.3 @@ -9,7 +9,7 @@
    51.4  goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
    51.5  by (list.induct_tac "xs" 1);
    51.6  by (Asm_simp_tac 1);
    51.7 -by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    51.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
    51.9  qed "mset_ins";
   51.10  Addsimps [mset_ins];
   51.11  
   51.12 @@ -20,7 +20,7 @@
   51.13  
   51.14  goal thy "set(ins f x xs) = insert x (set xs)";
   51.15  by (asm_simp_tac (!simpset addsimps [set_via_mset]
   51.16 -                           setloop (split_tac [expand_if])) 1);
   51.17 +                           addsplits [expand_if]) 1);
   51.18  by (Fast_tac 1);
   51.19  qed "set_ins";
   51.20  Addsimps [set_ins];
   51.21 @@ -28,7 +28,7 @@
   51.22  val prems = goalw InSort.thy [total_def,transf_def]
   51.23    "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
   51.24  by (list.induct_tac "xs" 1);
   51.25 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   51.26 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   51.27  by (cut_facts_tac prems 1);
   51.28  by (Fast_tac 1);
   51.29  qed "sorted_ins";
    52.1 --- a/src/HOL/ex/Primes.ML	Fri Oct 17 15:23:14 1997 +0200
    52.2 +++ b/src/HOL/ex/Primes.ML	Fri Oct 17 15:25:12 1997 +0200
    52.3 @@ -36,7 +36,7 @@
    52.4  
    52.5  goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
    52.6  by (rtac (gcd_eq RS trans) 1);
    52.7 -by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
    52.8 +by (asm_simp_tac (!simpset addsplits [expand_if]) 1);
    52.9  qed "gcd_less_0";
   52.10  Addsimps [gcd_0, gcd_less_0];
   52.11  
    53.1 --- a/src/HOL/ex/Qsort.ML	Fri Oct 17 15:23:14 1997 +0200
    53.2 +++ b/src/HOL/ex/Qsort.ML	Fri Oct 17 15:25:12 1997 +0200
    53.3 @@ -26,7 +26,7 @@
    53.4  
    53.5  goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
    53.6  by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
    53.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    53.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
    53.9  qed "qsort_permutes";
   53.10  
   53.11  goal Qsort.thy "set(qsort le xs) = set xs";
   53.12 @@ -37,7 +37,7 @@
   53.13  goal List.thy
   53.14    "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
   53.15  by (list.induct_tac "xs" 1);
   53.16 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   53.17 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   53.18  qed"Ball_set_filter";
   53.19  Addsimps [Ball_set_filter];
   53.20  
    54.1 --- a/src/HOL/ex/Recdef.ML	Fri Oct 17 15:23:14 1997 +0200
    54.2 +++ b/src/HOL/ex/Recdef.ML	Fri Oct 17 15:25:12 1997 +0200
    54.3 @@ -13,7 +13,7 @@
    54.4  
    54.5  goal thy "(x mem qsort (ord,l)) = (x mem l)";
    54.6  by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
    54.7 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
    54.8 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    54.9  by (Blast_tac 1);
   54.10  qed "qsort_mem_stable";
   54.11  
    55.1 --- a/src/HOL/ex/Sorting.ML	Fri Oct 17 15:23:14 1997 +0200
    55.2 +++ b/src/HOL/ex/Sorting.ML	Fri Oct 17 15:25:12 1997 +0200
    55.3 @@ -8,20 +8,20 @@
    55.4  
    55.5  goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
    55.6  by (list.induct_tac "xs" 1);
    55.7 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    55.8 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
    55.9  qed "mset_append";
   55.10  
   55.11  goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
   55.12  \                     mset xs x";
   55.13  by (list.induct_tac "xs" 1);
   55.14 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   55.15 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   55.16  qed "mset_compl_add";
   55.17  
   55.18  Addsimps [mset_append, mset_compl_add];
   55.19  
   55.20  goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
   55.21  by (list.induct_tac "xs" 1);
   55.22 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   55.23 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   55.24  by (Fast_tac 1);
   55.25  qed "set_via_mset";
   55.26  
   55.27 @@ -30,7 +30,7 @@
   55.28  val prems = goalw Sorting.thy [transf_def]
   55.29    "transf(le) ==> sorted1 le xs = sorted le xs";
   55.30  by (list.induct_tac "xs" 1);
   55.31 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_list_case]))));
   55.32 +by (ALLGOALS(asm_simp_tac (!simpset addsplits [expand_list_case])));
   55.33  by (cut_facts_tac prems 1);
   55.34  by (Fast_tac 1);
   55.35  qed "sorted1_is_sorted";
    56.1 --- a/src/HOL/ex/set.ML	Fri Oct 17 15:23:14 1997 +0200
    56.2 +++ b/src/HOL/ex/set.ML	Fri Oct 17 15:25:12 1997 +0200
    56.3 @@ -77,7 +77,7 @@
    56.4  
    56.5  goalw Lfp.thy [image_def]
    56.6      "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
    56.7 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    56.8 +by (simp_tac (!simpset addsplits [expand_if]) 1);
    56.9  by (Blast_tac 1);
   56.10  qed "range_if_then_else";
   56.11  
    57.1 --- a/src/HOL/simpdata.ML	Fri Oct 17 15:23:14 1997 +0200
    57.2 +++ b/src/HOL/simpdata.ML	Fri Oct 17 15:25:12 1997 +0200
    57.3 @@ -328,6 +328,9 @@
    57.4  fun split_inside_tac splits = mktac (map mk_meta_eq splits)
    57.5  end;
    57.6  
    57.7 +infix 4 addsplits;
    57.8 +fun ss addsplits splits = ss addloop (split_tac splits);
    57.9 +
   57.10  
   57.11  qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
   57.12    (fn _ => [split_tac [expand_if] 1, blast_tac HOL_cs 1]);