Removed `addsplits [expand_if]'
authornipkow
Sat Mar 07 16:29:29 1998 +0100 (1998-03-07)
changeset 468674a12e86b20b
parent 4685 9259feeeb2c8
child 4687 8cec457a8961
Removed `addsplits [expand_if]'
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/Public.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/IMP/Hoare.ML
src/HOL/Induct/Com.ML
src/HOL/Induct/LFilter.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/Lex/Regset_of_auto.ML
src/HOL/List.ML
src/HOL/Map.ML
src/HOL/MiniML/Generalize.ML
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/MiniML.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/W.ML
src/HOL/Nat.ML
src/HOL/NatDef.ML
src/HOL/Ord.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/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
     1.1 --- a/src/HOL/Arith.ML	Fri Mar 06 18:25:28 1998 +0100
     1.2 +++ b/src/HOL/Arith.ML	Sat Mar 07 16:29:29 1998 +0100
     1.3 @@ -433,12 +433,11 @@
     1.4  qed "less_imp_diff_positive";
     1.5  
     1.6  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
     1.7 -by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
     1.8 -                       addsplits [expand_if]) 1);
     1.9 +by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]) 1);
    1.10  qed "if_Suc_diff_n";
    1.11  
    1.12  goal Arith.thy "Suc(m)-n <= Suc(m-n)";
    1.13 -by (simp_tac (simpset() addsimps [if_Suc_diff_n] addsplits [expand_if]) 1);
    1.14 +by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
    1.15  qed "diff_Suc_le_Suc_diff";
    1.16  
    1.17  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
     2.1 --- a/src/HOL/Auth/Event.ML	Fri Mar 06 18:25:28 1998 +0100
     2.2 +++ b/src/HOL/Auth/Event.ML	Sat Mar 07 16:29:29 1998 +0100
     2.3 @@ -46,22 +46,20 @@
     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() addsplits [expand_if]) 1);
     2.8 +by (Simp_tac 1);
     2.9  by (Fast_tac 1);
    2.10  qed "spies_subset_spies_Notes";
    2.11  
    2.12  (*Spy sees all traffic*)
    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() addsplits [expand_event_case, expand_if])));
    2.17 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    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() addsplits [expand_event_case, expand_if])));
    2.25 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    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 +78,7 @@
    2.30  by (induct_tac "evs" 1);
    2.31  by (ALLGOALS (asm_simp_tac
    2.32  	      (simpset() addsimps [parts_insert_spies]
    2.33 -	                addsplits [expand_event_case, expand_if])));
    2.34 +	                addsplits [expand_event_case])));
    2.35  by (ALLGOALS Blast_tac);
    2.36  qed "parts_spies_subset_used";
    2.37  
    2.38 @@ -91,7 +89,7 @@
    2.39  by (induct_tac "evs" 1);
    2.40  by (ALLGOALS (asm_simp_tac
    2.41  	      (simpset() addsimps [parts_insert_spies]
    2.42 -	                addsplits [expand_event_case, expand_if])));
    2.43 +	                addsplits [expand_event_case])));
    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 Mar 06 18:25:28 1998 +0100
     3.2 +++ b/src/HOL/Auth/Message.ML	Sat Mar 07 16:29:29 1998 +0100
     3.3 @@ -896,7 +896,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() addsplits [expand_if]) 1,
     3.8 +       Simp_tac 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 Mar 06 18:25:28 1998 +0100
     4.2 +++ b/src/HOL/Auth/NS_Public.ML	Sat Mar 07 16:29:29 1998 +0100
     4.3 @@ -116,9 +116,9 @@
     4.4  
     4.5  
     4.6  (*Tactic for proving secrecy theorems*)
     4.7 -fun analz_induct_tac i = 
     4.8 +fun analz_induct_tac i =
     4.9      etac ns_public.induct i   THEN
    4.10 -    ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
    4.11 +    ALLGOALS Asm_simp_tac;
    4.12  
    4.13  
    4.14  (*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 Mar 06 18:25:28 1998 +0100
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Sat Mar 07 16:29:29 1998 +0100
     5.3 @@ -122,7 +122,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 (simpset() addsplits [expand_if]));
     5.8 +    ALLGOALS Asm_simp_tac;
     5.9  
    5.10  
    5.11  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
     6.1 --- a/src/HOL/Auth/Public.ML	Fri Mar 06 18:25:28 1998 +0100
     6.2 +++ b/src/HOL/Auth/Public.ML	Sat Mar 07 16:29:29 1998 +0100
     6.3 @@ -76,7 +76,7 @@
     6.4  by (induct_tac "evs" 1);
     6.5  by (ALLGOALS (asm_simp_tac
     6.6  	      (simpset() addsimps [imageI, spies_Cons]
     6.7 -	                addsplits [expand_event_case, expand_if])));
     6.8 +	                addsplits [expand_event_case])));
     6.9  qed_spec_mp "spies_pubK";
    6.10  
    6.11  (*Spy sees private keys of bad agents!*)
    6.12 @@ -84,7 +84,7 @@
    6.13  by (induct_tac "evs" 1);
    6.14  by (ALLGOALS (asm_simp_tac
    6.15  	      (simpset() addsimps [imageI, spies_Cons]
    6.16 -	                addsplits [expand_event_case, expand_if])));
    6.17 +	                addsplits [expand_event_case])));
    6.18  qed "Spy_spies_bad";
    6.19  
    6.20  AddIffs [spies_pubK, spies_pubK RS analz.Inj];
    6.21 @@ -132,7 +132,7 @@
    6.22  by (res_inst_tac [("x","0")] exI 1);
    6.23  by (ALLGOALS (asm_simp_tac
    6.24  	      (simpset() addsimps [used_Cons]
    6.25 -			addsplits [expand_event_case, expand_if])));
    6.26 +			addsplits [expand_event_case])));
    6.27  by Safe_tac;
    6.28  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
    6.29  by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
    6.30 @@ -177,6 +177,5 @@
    6.31                addsimps [image_insert RS sym, image_Un RS sym,
    6.32  			rangeI, 
    6.33  			insert_Key_singleton, 
    6.34 -			insert_Key_image, Un_assoc RS sym]
    6.35 -              addsplits [expand_if];
    6.36 +			insert_Key_image, Un_assoc RS sym];
    6.37  
     7.1 --- a/src/HOL/Auth/Shared.ML	Fri Mar 06 18:25:28 1998 +0100
     7.2 +++ b/src/HOL/Auth/Shared.ML	Sat Mar 07 16:29:29 1998 +0100
     7.3 @@ -51,7 +51,7 @@
     7.4  by (induct_tac "evs" 1);
     7.5  by (ALLGOALS (asm_simp_tac
     7.6  	      (simpset() addsimps [imageI, spies_Cons]
     7.7 -	                addsplits [expand_event_case, expand_if])));
     7.8 +	                addsplits [expand_event_case])));
     7.9  qed "Spy_spies_bad";
    7.10  
    7.11  AddSIs [Spy_spies_bad];
    7.12 @@ -125,7 +125,7 @@
    7.13  by (res_inst_tac [("x","0")] exI 1);
    7.14  by (ALLGOALS (asm_simp_tac
    7.15  	      (simpset() addsimps [used_Cons]
    7.16 -			addsplits [expand_event_case, expand_if])));
    7.17 +			addsplits [expand_event_case])));
    7.18  by Safe_tac;
    7.19  by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
    7.20  by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
    7.21 @@ -246,8 +246,7 @@
    7.22                           analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
    7.23                           insert_Key_singleton, subset_Compl_range,
    7.24                           Key_not_used, insert_Key_image, Un_assoc RS sym]
    7.25 -                        @disj_comms)
    7.26 -              addsplits [expand_if];
    7.27 +                        @disj_comms);
    7.28  
    7.29  (*Lemma for the trivial direction of the if-and-only-if*)
    7.30  goal thy  
     8.1 --- a/src/HOL/Auth/TLS.ML	Fri Mar 06 18:25:28 1998 +0100
     8.2 +++ b/src/HOL/Auth/TLS.ML	Sat Mar 07 16:29:29 1998 +0100
     8.3 @@ -145,7 +145,7 @@
     8.4      REPEAT (FIRSTGOAL analz_mono_contra_tac)
     8.5      THEN 
     8.6      fast_tac (claset() addss (simpset())) i THEN
     8.7 -    ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
     8.8 +    ALLGOALS Asm_simp_tac;
     8.9  
    8.10  
    8.11  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    8.12 @@ -193,14 +193,12 @@
    8.13      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
    8.14      ALLGOALS (asm_simp_tac 
    8.15                (simpset() addcongs [if_weak_cong]
    8.16 -                         addsimps (expand_ifs@pushes)
    8.17 -                         addsplits [expand_if]))  THEN
    8.18 +                         addsimps (expand_ifs@pushes)))  THEN
    8.19      (*Remove instances of pubK B:  the Spy already knows all public keys.
    8.20        Combining the two simplifier calls makes them run extremely slowly.*)
    8.21      ALLGOALS (asm_simp_tac 
    8.22                (simpset() addcongs [if_weak_cong]
    8.23 -			 addsimps [insert_absorb]
    8.24 -                         addsplits [expand_if]));
    8.25 +			 addsimps [insert_absorb]));
    8.26  
    8.27  
    8.28  (*** Properties of items found in Notes ***)
     9.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Mar 06 18:25:28 1998 +0100
     9.2 +++ b/src/HOL/Auth/Yahalom2.ML	Sat Mar 07 16:29:29 1998 +0100
     9.3 @@ -216,8 +216,7 @@
     9.4  by (ALLGOALS
     9.5      (asm_simp_tac 
     9.6       (simpset() addsimps expand_ifs
     9.7 -	        addsimps [analz_insert_eq, analz_insert_freshK]
     9.8 -                addsplits [expand_if])));
     9.9 +	        addsimps [analz_insert_eq, analz_insert_freshK])));
    9.10  (*Oops*)
    9.11  by (blast_tac (claset() addDs [unique_session_keys]) 3);
    9.12  (*YM3*)
    10.1 --- a/src/HOL/Divides.ML	Fri Mar 06 18:25:28 1998 +0100
    10.2 +++ b/src/HOL/Divides.ML	Sat Mar 07 16:29:29 1998 +0100
    10.3 @@ -229,7 +229,7 @@
    10.4  goal thy "!!k b. b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
    10.5  by (subgoal_tac "k mod 2 < 2" 1);
    10.6  by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
    10.7 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    10.8 +by (Asm_simp_tac 1);
    10.9  by Safe_tac;
   10.10  qed "mod2_cases";
   10.11  
    11.1 --- a/src/HOL/Finite.ML	Fri Mar 06 18:25:28 1998 +0100
    11.2 +++ b/src/HOL/Finite.ML	Sat Mar 07 16:29:29 1998 +0100
    11.3 @@ -257,7 +257,7 @@
    11.4     by (SELECT_GOAL Safe_tac 1);
    11.5     by (res_inst_tac [("x","k")] exI 1);
    11.6     by (Asm_simp_tac 1);
    11.7 -  by (simp_tac (simpset() addsplits [expand_if]) 1);
    11.8 +  by (Simp_tac 1);
    11.9    by (Blast_tac 1);
   11.10   by (dtac sym 1);
   11.11   by (rotate_tac ~1 1);
   11.12 @@ -271,7 +271,7 @@
   11.13    by (SELECT_GOAL Safe_tac 1);
   11.14    by (res_inst_tac [("x","k")] exI 1);
   11.15    by (Asm_simp_tac 1);
   11.16 - by (simp_tac (simpset() addsplits [expand_if]) 1);
   11.17 + by (Simp_tac 1);
   11.18   by (Blast_tac 1);
   11.19  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
   11.20  by (SELECT_GOAL Safe_tac 1);
   11.21 @@ -285,7 +285,7 @@
   11.22   by (SELECT_GOAL Safe_tac 1);
   11.23   by (res_inst_tac [("x","k")] exI 1);
   11.24   by (Asm_simp_tac 1);
   11.25 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   11.26 +by (Simp_tac 1);
   11.27  by (Blast_tac 1);
   11.28  val lemma = result();
   11.29  
   11.30 @@ -341,9 +341,7 @@
   11.31  goal Finite.thy "!!A B. [| finite A; finite B |]\
   11.32  \                       ==> A Int B = {} --> card(A Un B) = card A + card B";
   11.33  by (etac finite_induct 1);
   11.34 -by (ALLGOALS 
   11.35 -    (asm_simp_tac (simpset() addsimps [Int_insert_left]
   11.36 -	                    addsplits [expand_if])));
   11.37 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Int_insert_left])));
   11.38  qed_spec_mp "card_Un_disjoint";
   11.39  
   11.40  goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
    12.1 --- a/src/HOL/IMP/Hoare.ML	Fri Mar 06 18:25:28 1998 +0100
    12.2 +++ b/src/HOL/IMP/Hoare.ML	Sat Mar 07 16:29:29 1998 +0100
    12.3 @@ -61,13 +61,13 @@
    12.4  (*Not suitable for rewriting: LOOPS!*)
    12.5  goal Hoare.thy "wp (WHILE b DO c) Q s = \
    12.6  \                 (if b s then wp (c;WHILE b DO c) Q s else Q s)";
    12.7 -by (simp_tac (simpset() addsplits [expand_if]) 1);
    12.8 +by (Simp_tac 1);
    12.9  qed "wp_While_if";
   12.10  
   12.11  goal thy
   12.12    "wp (WHILE b DO c) Q s = \
   12.13  \  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
   12.14 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   12.15 +by (Simp_tac 1);
   12.16  by (rtac iffI 1);
   12.17   by (rtac weak_coinduct 1);
   12.18    by (etac CollectI 1);
    13.1 --- a/src/HOL/Induct/Com.ML	Fri Mar 06 18:25:28 1998 +0100
    13.2 +++ b/src/HOL/Induct/Com.ML	Sat Mar 07 16:29:29 1998 +0100
    13.3 @@ -54,7 +54,7 @@
    13.4  
    13.5  goalw thy [assign_def] "s[s x/x] = s";
    13.6  by (rtac ext 1);
    13.7 -by (simp_tac (simpset() addsplits [expand_if]) 1);
    13.8 +by (Simp_tac 1);
    13.9  qed "assign_triv";
   13.10  
   13.11  Addsimps [assign_same, assign_different, assign_triv];
    14.1 --- a/src/HOL/Induct/LFilter.ML	Fri Mar 06 18:25:28 1998 +0100
    14.2 +++ b/src/HOL/Induct/LFilter.ML	Sat Mar 07 16:29:29 1998 +0100
    14.3 @@ -98,7 +98,7 @@
    14.4  Addsimps [find_LCons_seek];
    14.5  
    14.6  goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
    14.7 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    14.8 +by (Asm_simp_tac 1);
    14.9  qed "find_LCons";
   14.10  
   14.11  
   14.12 @@ -148,8 +148,7 @@
   14.13  
   14.14  goal thy "lfilter p (LCons x l) = \
   14.15  \         (if p x then LCons x (lfilter p l) else lfilter p l)";
   14.16 -by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
   14.17 -                            addsplits [expand_if]) 1);
   14.18 +by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]) 1);
   14.19  qed "lfilter_LCons";
   14.20  
   14.21  AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   14.22 @@ -193,7 +192,7 @@
   14.23  
   14.24  goal thy "lfilter p (lfilter p l) = lfilter p l";
   14.25  by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   14.26 -by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
   14.27 +by (ALLGOALS Simp_tac);
   14.28  by Safe_tac;
   14.29  (*Cases: p x is true or false*)
   14.30  by (rtac (lfilter_cases RS disjE) 1);
   14.31 @@ -250,7 +249,7 @@
   14.32  \              ==> l'' = LCons y l' --> \
   14.33  \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
   14.34  by (etac findRel.induct 1);
   14.35 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   14.36 +by (ALLGOALS Asm_simp_tac);
   14.37  by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
   14.38  qed_spec_mp "findRel_conj_lfilter";
   14.39  
   14.40 @@ -291,7 +290,7 @@
   14.41  
   14.42  goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
   14.43  by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   14.44 -by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
   14.45 +by (ALLGOALS Simp_tac);
   14.46  by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
   14.47  qed "lfilter_conj";
   14.48  
   14.49 @@ -329,7 +328,7 @@
   14.50  
   14.51  goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
   14.52  by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   14.53 -by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
   14.54 +by (ALLGOALS Simp_tac);
   14.55  by Safe_tac;
   14.56  by (case_tac "lmap f l : Domain (findRel p)" 1);
   14.57  by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
    15.1 --- a/src/HOL/Induct/Mutil.ML	Fri Mar 06 18:25:28 1998 +0100
    15.2 +++ b/src/HOL/Induct/Mutil.ML	Sat Mar 07 16:29:29 1998 +0100
    15.3 @@ -92,7 +92,7 @@
    15.4  goalw thy [evnodd_def]
    15.5      "evnodd (insert (i,j) C) b = \
    15.6  \      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
    15.7 -by (simp_tac (simpset() addsplits [expand_if]) 1);
    15.8 +by (Simp_tac 1);
    15.9  by (Blast_tac 1);
   15.10  qed "evnodd_insert";
   15.11  
   15.12 @@ -107,8 +107,7 @@
   15.13  by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
   15.14  by (REPEAT_FIRST assume_tac);
   15.15  (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
   15.16 -by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc] 
   15.17 -                          addsplits [expand_if]) 1
   15.18 +by (REPEAT (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1
   15.19             THEN Blast_tac 1));
   15.20  qed "domino_singleton";
   15.21  
    16.1 --- a/src/HOL/Induct/Perm.ML	Fri Mar 06 18:25:28 1998 +0100
    16.2 +++ b/src/HOL/Induct/Perm.ML	Sat Mar 07 16:29:29 1998 +0100
    16.3 @@ -41,7 +41,7 @@
    16.4  goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
    16.5  by (etac perm.induct 1);
    16.6  by (Fast_tac 4);
    16.7 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    16.8 +by (ALLGOALS Asm_simp_tac);
    16.9  val perm_mem_lemma = result();
   16.10  
   16.11  bind_thm ("perm_mem", perm_mem_lemma RS mp);
    17.1 --- a/src/HOL/Induct/PropLog.ML	Fri Mar 06 18:25:28 1998 +0100
    17.2 +++ b/src/HOL/Induct/PropLog.ML	Sat Mar 07 16:29:29 1998 +0100
    17.3 @@ -141,9 +141,7 @@
    17.4    we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
    17.5  goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
    17.6  by (PropLog.pl.induct_tac "p" 1);
    17.7 -by (Simp_tac 1);
    17.8 -by (simp_tac (simpset() addsplits [expand_if]) 1);
    17.9 -by (Simp_tac 1);
   17.10 +by (ALLGOALS Simp_tac);
   17.11  by (Fast_tac 1);
   17.12  qed "hyps_Diff";
   17.13  
   17.14 @@ -151,9 +149,7 @@
   17.15    we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
   17.16  goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
   17.17  by (PropLog.pl.induct_tac "p" 1);
   17.18 -by (Simp_tac 1);
   17.19 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   17.20 -by (Simp_tac 1);
   17.21 +by (ALLGOALS Simp_tac);
   17.22  by (Fast_tac 1);
   17.23  qed "hyps_insert";
   17.24  
   17.25 @@ -174,7 +170,7 @@
   17.26  
   17.27  goal PropLog.thy "hyps p t <= (UN v. {#v, #v->false})";
   17.28  by (PropLog.pl.induct_tac "p" 1);
   17.29 -by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
   17.30 +by (ALLGOALS Simp_tac);
   17.31  by (Blast_tac 1);
   17.32  qed "hyps_subset";
   17.33  
    18.1 --- a/src/HOL/Induct/SList.ML	Fri Mar 06 18:25:28 1998 +0100
    18.2 +++ b/src/HOL/Induct/SList.ML	Sat Mar 07 16:29:29 1998 +0100
    18.3 @@ -317,12 +317,12 @@
    18.4  
    18.5  goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
    18.6  by (list_ind_tac "xs" 1);
    18.7 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
    18.8 +by (ALLGOALS Asm_simp_tac);
    18.9  qed "mem_append2";
   18.10  
   18.11  goal SList.thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   18.12  by (list_ind_tac "xs" 1);
   18.13 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   18.14 +by (ALLGOALS Asm_simp_tac);
   18.15  qed "mem_filter2";
   18.16  
   18.17  
    19.1 --- a/src/HOL/Integ/Bin.ML	Fri Mar 06 18:25:28 1998 +0100
    19.2 +++ b/src/HOL/Integ/Bin.ML	Sat Mar 07 16:29:29 1998 +0100
    19.3 @@ -100,8 +100,6 @@
    19.4  
    19.5  (**** The carry/borrow functions, bin_succ and bin_pred ****)
    19.6  
    19.7 -val if_ss = simpset() addsplits [expand_if];
    19.8 -
    19.9  
   19.10  (**** integ_of_bin ****)
   19.11  
   19.12 @@ -109,26 +107,26 @@
   19.13  qed_goal "integ_of_bin_norm_Bcons" Bin.thy
   19.14      "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
   19.15   (fn _ =>[(bin.induct_tac "w" 1),
   19.16 -          (ALLGOALS(simp_tac if_ss)) ]);
   19.17 +          (ALLGOALS Simp_tac) ]);
   19.18  
   19.19  qed_goal "integ_of_bin_succ" Bin.thy
   19.20      "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
   19.21   (fn _ =>[(rtac bin.induct 1),
   19.22            (ALLGOALS(asm_simp_tac 
   19.23 -                    (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
   19.24 +                    (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
   19.25  
   19.26  qed_goal "integ_of_bin_pred" Bin.thy
   19.27      "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
   19.28   (fn _ =>[(rtac bin.induct 1),
   19.29            (ALLGOALS(asm_simp_tac
   19.30 -                  (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
   19.31 +                  (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
   19.32  
   19.33  qed_goal "integ_of_bin_minus" Bin.thy
   19.34      "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
   19.35   (fn _ =>[(rtac bin.induct 1),
   19.36            (Simp_tac 1),
   19.37            (Simp_tac 1),
   19.38 -          (asm_simp_tac (if_ss
   19.39 +          (asm_simp_tac (simpset()
   19.40                           delsimps [pred_Plus,pred_Minus,pred_Bcons]
   19.41                           addsimps [integ_of_bin_succ,integ_of_bin_pred,
   19.42                                     zadd_assoc]) 1)]);
   19.43 @@ -143,16 +141,16 @@
   19.44  goal Bin.thy
   19.45      "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
   19.46  by (bin.induct_tac "v" 1);
   19.47 -by (simp_tac (if_ss addsimps bin_add_simps) 1);
   19.48 -by (simp_tac (if_ss addsimps bin_add_simps) 1);
   19.49 +by (simp_tac (simpset() addsimps bin_add_simps) 1);
   19.50 +by (simp_tac (simpset() addsimps bin_add_simps) 1);
   19.51  by (rtac allI 1);
   19.52  by (bin.induct_tac "w" 1);
   19.53 -by (asm_simp_tac (if_ss addsimps (bin_add_simps)) 1);
   19.54 -by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
   19.55 +by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1);
   19.56 +by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
   19.57  by (cut_inst_tac [("P","bool")] True_or_False 1);
   19.58  by (etac disjE 1);
   19.59 -by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
   19.60 -by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
   19.61 +by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
   19.62 +by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
   19.63  val integ_of_bin_add_lemma = result();
   19.64  
   19.65  goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
   19.66 @@ -165,12 +163,12 @@
   19.67  
   19.68  goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
   19.69  by (bin.induct_tac "v" 1);
   19.70 -by (simp_tac (if_ss addsimps bin_mult_simps) 1);
   19.71 -by (simp_tac (if_ss addsimps bin_mult_simps) 1);
   19.72 +by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   19.73 +by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   19.74  by (cut_inst_tac [("P","bool")] True_or_False 1);
   19.75  by (etac disjE 1);
   19.76 -by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
   19.77 -by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ 
   19.78 +by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
   19.79 +by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ 
   19.80                                    zadd_ac)) 1);
   19.81  qed "integ_of_bin_mult";
   19.82  
    20.1 --- a/src/HOL/Lambda/Eta.ML	Fri Mar 06 18:25:28 1998 +0100
    20.2 +++ b/src/HOL/Lambda/Eta.ML	Sat Mar 07 16:29:29 1998 +0100
    20.3 @@ -50,7 +50,7 @@
    20.4  by (Blast_tac 2);
    20.5  by (asm_full_simp_tac (addsplit (simpset())) 2);
    20.6  by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
    20.7 -                      addsplits [expand_if,expand_nat_case]) 1);
    20.8 +                      addsplits [expand_nat_case]) 1);
    20.9  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   20.10  by (ALLGOALS trans_tac);
   20.11  qed "free_subst";
   20.12 @@ -168,7 +168,7 @@
   20.13  
   20.14  goal Eta.thy "!i. (~free s i) = (? t. s = lift t i)";
   20.15  by (dB.induct_tac "s" 1);
   20.16 -  by (simp_tac (simpset() addsplits [expand_if]) 1);
   20.17 +  by (Simp_tac 1);
   20.18    by (SELECT_GOAL(safe_tac HOL_cs)1);
   20.19     by (etac nat_neqE 1);
   20.20      by (res_inst_tac [("x","Var nat")] exI 1);
   20.21 @@ -179,7 +179,7 @@
   20.22     by (assume_tac 2);
   20.23    by (etac thin_rl 1);
   20.24    by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   20.25 -    by (simp_tac (simpset() addsplits [expand_if]) 1);
   20.26 +    by (Simp_tac 1);
   20.27      by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
   20.28     by (Simp_tac 1);
   20.29    by (Simp_tac 1);
   20.30 @@ -195,7 +195,7 @@
   20.31   by (etac exE 1);
   20.32   by (etac rev_mp 1);
   20.33   by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   20.34 -   by (simp_tac (simpset() addsplits [expand_if]) 1);
   20.35 +   by (Simp_tac 1);
   20.36    by (Simp_tac 1);
   20.37    by (Blast_tac 1);
   20.38   by (Simp_tac 1);
   20.39 @@ -209,7 +209,7 @@
   20.40  by (etac exE 1);
   20.41  by (etac rev_mp 1);
   20.42  by (res_inst_tac [("dB","t")] dB_case_distinction 1);
   20.43 -  by (simp_tac (simpset() addsplits [expand_if]) 1);
   20.44 +  by (Simp_tac 1);
   20.45   by (Simp_tac 1);
   20.46  by (Simp_tac 1);
   20.47  by (Blast_tac 1);
    21.1 --- a/src/HOL/Lambda/Lambda.ML	Fri Mar 06 18:25:28 1998 +0100
    21.2 +++ b/src/HOL/Lambda/Lambda.ML	Sat Mar 07 16:29:29 1998 +0100
    21.3 @@ -46,6 +46,7 @@
    21.4  (*** subst and lift ***)
    21.5  
    21.6  fun addsplit ss = ss addsimps [subst_Var]
    21.7 +                     delsplits [expand_if]
    21.8                       setloop (split_inside_tac [expand_if]);
    21.9  
   21.10  goal Lambda.thy "(Var k)[u/k] = u";
   21.11 @@ -66,8 +67,7 @@
   21.12  goal Lambda.thy
   21.13    "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
   21.14  by (dB.induct_tac "t" 1);
   21.15 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]
   21.16 -                                    addSolver cut_trans_tac)));
   21.17 +by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
   21.18  by (safe_tac HOL_cs);
   21.19  by (ALLGOALS trans_tac);
   21.20  qed_spec_mp "lift_lift";
   21.21 @@ -76,7 +76,7 @@
   21.22  \         lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
   21.23  by (dB.induct_tac "t" 1);
   21.24  by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
   21.25 -                                addsplits [expand_if,expand_nat_case]
   21.26 +                                addsplits [expand_nat_case]
   21.27                                  addSolver cut_trans_tac)));
   21.28  by (safe_tac HOL_cs);
   21.29  by (ALLGOALS trans_tac);
   21.30 @@ -88,7 +88,6 @@
   21.31  \         lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
   21.32  by (dB.induct_tac "t" 1);
   21.33  by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
   21.34 -                                addsplits [expand_if]
   21.35                                  addSolver cut_trans_tac)));
   21.36  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   21.37  by (ALLGOALS trans_tac);
   21.38 @@ -96,7 +95,7 @@
   21.39  
   21.40  goal Lambda.thy "!k s. (lift t k)[s/k] = t";
   21.41  by (dB.induct_tac "t" 1);
   21.42 -by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if])));
   21.43 +by (ALLGOALS Asm_full_simp_tac);
   21.44  qed "subst_lift";
   21.45  Addsimps [subst_lift];
   21.46  
   21.47 @@ -106,7 +105,9 @@
   21.48  by (dB.induct_tac "t" 1);
   21.49  by (ALLGOALS(asm_simp_tac
   21.50        (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
   21.51 -                addsplits [expand_if,expand_nat_case]
   21.52 +                 delsplits [expand_if]
   21.53 +                 addsplits [expand_nat_case]
   21.54 +                 addloop ("if",split_inside_tac[expand_if])
   21.55                  addSolver cut_trans_tac)));
   21.56  by (safe_tac (HOL_cs addSEs [nat_neqE]));
   21.57  by (ALLGOALS trans_tac);
    22.1 --- a/src/HOL/Lex/AutoChopper.ML	Fri Mar 06 18:25:28 1998 +0100
    22.2 +++ b/src/HOL/Lex/AutoChopper.ML	Sat Mar 07 16:29:29 1998 +0100
    22.3 @@ -18,7 +18,7 @@
    22.4  goal AutoChopper.thy "!st us p y ys. acc xs st (ys@[y]) us p A ~= ([],zs)";
    22.5  by (list.induct_tac "xs" 1);
    22.6  by (Simp_tac 1);
    22.7 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    22.8 +by (Asm_simp_tac 1);
    22.9  val accept_not_Nil = result() repeat_RS spec;
   22.10  Addsimps [accept_not_Nil];
   22.11  
   22.12 @@ -27,7 +27,7 @@
   22.13  \        zs = ys & (!ys. ys ~= [] & ys<=xs --> ~fin A (nexts A st ys))";
   22.14  by (list.induct_tac "xs" 1);
   22.15  by (simp_tac (simpset() addcongs [conj_cong]) 1);
   22.16 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   22.17 +by (Simp_tac 1);
   22.18  by (strip_tac 1);
   22.19  by (rtac conjI 1);
   22.20  by (Fast_tac 1);
   22.21 @@ -53,17 +53,17 @@
   22.22  \    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
   22.23  \    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
   22.24  by (list.induct_tac "xs" 1);
   22.25 - by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   22.26 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   22.27 + by (simp_tac (simpset() addcongs [conj_cong]) 1);
   22.28 +by (Asm_simp_tac 1);
   22.29  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   22.30  by (rename_tac "vss lrst" 1);  
   22.31 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   22.32 +by (Asm_simp_tac 1);
   22.33  by (res_inst_tac[("xs","vss")] list_eq_cases 1);
   22.34   by (hyp_subst_tac 1);
   22.35   by (Simp_tac 1);
   22.36   by (fast_tac (claset() addSDs [no_acc]) 1);
   22.37  by (hyp_subst_tac 1);
   22.38 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   22.39 +by (Asm_simp_tac 1);
   22.40  val step2_a = (result() repeat_RS spec) RS mp;
   22.41  
   22.42  
   22.43 @@ -73,11 +73,11 @@
   22.44  \     (if acc_prefix A st xs \
   22.45  \      then ys ~= [] \
   22.46  \      else ys ~= [] | (erk=[] & (l,rest) = (ys#yss,zs)))";
   22.47 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   22.48 +by (Simp_tac 1);
   22.49  by (list.induct_tac "xs" 1);
   22.50 - by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   22.51 + by (simp_tac (simpset() addcongs [conj_cong]) 1);
   22.52   by (Fast_tac 1);
   22.53 -by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   22.54 +by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
   22.55  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   22.56  by (rename_tac "vss lrst" 1);  
   22.57  by (Asm_simp_tac 1);
   22.58 @@ -96,11 +96,11 @@
   22.59  \     (if acc_prefix A st xs                   \
   22.60  \      then ? g. ys=r@g & fin A (nexts A st g)  \
   22.61  \      else (erk~=[] & erk=ys) | (erk=[] & (l,rest) = (ys#yss,zs)))";
   22.62 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   22.63 +by (Simp_tac 1);
   22.64  by (list.induct_tac "xs" 1);
   22.65 - by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   22.66 + by (simp_tac (simpset() addcongs [conj_cong]) 1);
   22.67   by (Fast_tac 1);
   22.68 -by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   22.69 +by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
   22.70  by (strip_tac 1);
   22.71  by (rtac conjI 1);
   22.72   by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   22.73 @@ -135,11 +135,11 @@
   22.74  \     (if acc_prefix A st xs       \
   22.75  \      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
   22.76  \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
   22.77 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   22.78 +by (Simp_tac 1);
   22.79  by (list.induct_tac "xs" 1);
   22.80 - by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   22.81 + by (simp_tac (simpset() addcongs [conj_cong]) 1);
   22.82   by (Fast_tac 1);
   22.83 -by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   22.84 +by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
   22.85  by (res_inst_tac [("p","acc list (start A) [] [] ([],list) A")] PairE 1);
   22.86  by (rename_tac "vss lrst" 1);  
   22.87  by (Asm_simp_tac 1);
   22.88 @@ -164,7 +164,7 @@
   22.89  by (Simp_tac 1);
   22.90  by (rtac trans 1);
   22.91   by (etac step2_a 1);
   22.92 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   22.93 +by (Simp_tac 1);
   22.94  val step2_d = (result() repeat_RS spec) RS mp;
   22.95  
   22.96  Delsimps [split_paired_All];
   22.97 @@ -174,11 +174,11 @@
   22.98  \  (if acc_prefix A st xs  \
   22.99  \   then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
  22.100  \   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
  22.101 -by (simp_tac (simpset() addsplits [expand_if]) 1);
  22.102 +by (Simp_tac 1);
  22.103  by (list.induct_tac "xs" 1);
  22.104 - by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
  22.105 + by (simp_tac (simpset() addcongs [conj_cong]) 1);
  22.106   by (Fast_tac 1);
  22.107 -by (asm_simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
  22.108 +by (asm_simp_tac (simpset() addcongs [conj_cong]) 1);
  22.109  by (strip_tac 1);
  22.110  by (case_tac "acc_prefix A (next A st a) list" 1);
  22.111   by (rtac conjI 1);
  22.112 @@ -225,18 +225,18 @@
  22.113  by (REPEAT(ares_tac [no_acc,allI,impI,conjI] 1));
  22.114   by (rtac mp 1);
  22.115    by (etac step2_b 2);
  22.116 - by (simp_tac (simpset() addsplits [expand_if]) 1);
  22.117 + by (Simp_tac 1);
  22.118  by (rtac conjI 1);
  22.119   by (rtac mp 1);
  22.120    by (etac step2_c 2);
  22.121 - by (simp_tac (simpset() addsplits [expand_if]) 1);
  22.122 + by (Simp_tac 1);
  22.123  by (rtac conjI 1);
  22.124 - by (asm_simp_tac (simpset() addsimps [step2_a] addsplits [expand_if]) 1);
  22.125 + by (asm_simp_tac (simpset() addsimps [step2_a]) 1);
  22.126  by (rtac conjI 1);
  22.127   by (rtac mp 1);
  22.128    by (etac step2_d 2);
  22.129 - by (simp_tac (simpset() addsplits [expand_if]) 1);
  22.130 + by (Simp_tac 1);
  22.131  by (rtac mp 1);
  22.132   by (etac step2_e 2);
  22.133 - by (simp_tac (simpset() addsplits [expand_if]) 1);
  22.134 + by (Simp_tac 1);
  22.135  qed"auto_chopper_is_auto_chopper";
    23.1 --- a/src/HOL/Lex/Regset_of_auto.ML	Fri Mar 06 18:25:28 1998 +0100
    23.2 +++ b/src/HOL/Lex/Regset_of_auto.ML	Sat Mar 07 16:29:29 1998 +0100
    23.3 @@ -23,15 +23,14 @@
    23.4  
    23.5  goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
    23.6  by (exhaust_tac "xs" 1);
    23.7 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    23.8 +by (ALLGOALS Asm_simp_tac);
    23.9  qed "butlast_empty";
   23.10  AddIffs [butlast_empty];
   23.11  
   23.12  goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
   23.13  by (induct_tac "xss" 1);
   23.14   by (Simp_tac 1);
   23.15 -by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
   23.16 -                           addsplits [expand_if]) 1);
   23.17 +by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps) 1);
   23.18  by (rtac conjI 1);
   23.19   by (Clarify_tac 1);
   23.20   by (rtac conjI 1);
   23.21 @@ -91,7 +90,7 @@
   23.22  by (res_inst_tac[("x","a#pref")]exI 1);
   23.23  by (res_inst_tac[("x","mids")]exI 1);
   23.24  by (res_inst_tac[("x","suf")]exI 1);
   23.25 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   23.26 +by (Asm_simp_tac 1);
   23.27  qed_spec_mp "decompose";
   23.28  
   23.29  goal thy "!i. length(trace A i xs) = length xs";
   23.30 @@ -137,7 +136,7 @@
   23.31  \ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
   23.32  by (induct_tac "xs" 1);
   23.33   by (Simp_tac 1);
   23.34 -by (asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
   23.35 +by (asm_simp_tac (simpset() addsimps [insert_commute]) 1);
   23.36  qed "set_trace_conv";
   23.37  
   23.38  goal thy
   23.39 @@ -157,8 +156,7 @@
   23.40   "!i j xs. xs : regset_of A i j k = \
   23.41  \          ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
   23.42  by (induct_tac "k" 1);
   23.43 - by (simp_tac (simpset() addcongs [conj_cong]
   23.44 -                        addsplits [expand_if,split_list_case]) 1);
   23.45 + by (simp_tac (simpset() addcongs [conj_cong] addsplits [split_list_case]) 1);
   23.46  by (strip_tac 1);
   23.47  by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
   23.48  by (rtac iffI 1);
   23.49 @@ -168,12 +166,10 @@
   23.50   by (Asm_full_simp_tac 1);
   23.51   by (subgoal_tac
   23.52        "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
   23.53 -  by (asm_simp_tac (simpset() addsplits [expand_if]
   23.54 -       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   23.55 +  by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   23.56   by (etac star.induct 1);
   23.57    by (Simp_tac 1);
   23.58 - by (asm_full_simp_tac (simpset() addsplits [expand_if]
   23.59 -       addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   23.60 + by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
   23.61  by (case_tac "k : set(butlast(trace A i xs))" 1);
   23.62   by (rtac disjI1 2);
   23.63   by (blast_tac (claset() addIs [lemma]) 2);
    24.1 --- a/src/HOL/List.ML	Fri Mar 06 18:25:28 1998 +0100
    24.2 +++ b/src/HOL/List.ML	Sat Mar 07 16:29:29 1998 +0100
    24.3 @@ -311,13 +311,13 @@
    24.4  
    24.5  goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
    24.6  by (induct_tac "xs" 1);
    24.7 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    24.8 +by (ALLGOALS Asm_simp_tac);
    24.9  qed "mem_append";
   24.10  Addsimps[mem_append];
   24.11  
   24.12  goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   24.13  by (induct_tac "xs" 1);
   24.14 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.15 +by (ALLGOALS Asm_simp_tac);
   24.16  qed "mem_filter";
   24.17  Addsimps[mem_filter];
   24.18  
   24.19 @@ -333,7 +333,7 @@
   24.20  
   24.21  goal thy "(x mem xs) = (x: set xs)";
   24.22  by (induct_tac "xs" 1);
   24.23 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.24 +by (ALLGOALS Asm_simp_tac);
   24.25  by (Blast_tac 1);
   24.26  qed "set_mem_eq";
   24.27  
   24.28 @@ -368,7 +368,7 @@
   24.29  
   24.30  goal thy "(x : set(filter P xs)) = (x : set xs & P x)";
   24.31  by (induct_tac "xs" 1);
   24.32 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.33 +by (ALLGOALS Asm_simp_tac);
   24.34  by(Blast_tac 1);
   24.35  qed "in_set_filter";
   24.36  Addsimps [in_set_filter];
   24.37 @@ -392,7 +392,7 @@
   24.38  
   24.39  goal thy "list_all P xs = (!x. x mem xs --> P(x))";
   24.40  by (induct_tac "xs" 1);
   24.41 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.42 +by (ALLGOALS Asm_simp_tac);
   24.43  by (Blast_tac 1);
   24.44  qed "list_all_mem_conv";
   24.45  
   24.46 @@ -403,7 +403,7 @@
   24.47  
   24.48  goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
   24.49  by (induct_tac "xs" 1);
   24.50 - by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.51 +by (ALLGOALS Asm_simp_tac);
   24.52  qed "filter_append";
   24.53  Addsimps [filter_append];
   24.54  
   24.55 @@ -421,7 +421,7 @@
   24.56  
   24.57  goal thy "length (filter P xs) <= length xs";
   24.58  by (induct_tac "xs" 1);
   24.59 - by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.60 +by (ALLGOALS Asm_simp_tac);
   24.61  qed "length_filter";
   24.62  
   24.63  
   24.64 @@ -512,7 +512,7 @@
   24.65  (* case 0 *)
   24.66  by (Asm_full_simp_tac 1);
   24.67  (* case Suc x *)
   24.68 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   24.69 +by (Asm_full_simp_tac 1);
   24.70  qed_spec_mp "nth_mem";
   24.71  Addsimps [nth_mem];
   24.72  
   24.73 @@ -565,42 +565,40 @@
   24.74  
   24.75  goal thy "last(xs@[x]) = x";
   24.76  by (induct_tac "xs" 1);
   24.77 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.78 +by (ALLGOALS Asm_simp_tac);
   24.79  qed "last_snoc";
   24.80  Addsimps [last_snoc];
   24.81  
   24.82  goal thy "butlast(xs@[x]) = xs";
   24.83  by (induct_tac "xs" 1);
   24.84 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   24.85 +by (ALLGOALS Asm_simp_tac);
   24.86  qed "butlast_snoc";
   24.87  Addsimps [butlast_snoc];
   24.88  
   24.89  goal thy "length(butlast xs) = length xs - 1";
   24.90 -by(res_inst_tac [("xs","xs")] snoc_induct 1);
   24.91 -by(ALLGOALS Asm_simp_tac);
   24.92 +by (res_inst_tac [("xs","xs")] snoc_induct 1);
   24.93 +by (ALLGOALS Asm_simp_tac);
   24.94  qed "length_butlast";
   24.95  Addsimps [length_butlast];
   24.96  
   24.97  goal thy
   24.98    "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   24.99  by (induct_tac "xs" 1);
  24.100 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
  24.101 +by (ALLGOALS Asm_simp_tac);
  24.102  qed_spec_mp "butlast_append";
  24.103  
  24.104  goal thy "x:set(butlast xs) --> x:set xs";
  24.105  by (induct_tac "xs" 1);
  24.106 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
  24.107 +by (ALLGOALS Asm_simp_tac);
  24.108  qed_spec_mp "in_set_butlastD";
  24.109  
  24.110  goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
  24.111 -by (asm_simp_tac (simpset() addsimps [butlast_append]
  24.112 -                          addsplits [expand_if]) 1);
  24.113 +by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
  24.114  by (blast_tac (claset() addDs [in_set_butlastD]) 1);
  24.115  qed "in_set_butlast_appendI1";
  24.116  
  24.117  goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
  24.118 -by (asm_simp_tac (simpset() addsimps [butlast_append]
  24.119 -                          addsplits [expand_if]) 1);
  24.120 +by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
  24.121  by (Clarify_tac 1);
  24.122  by (Full_simp_tac 1);
  24.123  qed "in_set_butlast_appendI2";
  24.124 @@ -751,15 +749,13 @@
  24.125  
  24.126  goal thy "takeWhile P xs @ dropWhile P xs = xs";
  24.127  by (induct_tac "xs" 1);
  24.128 - by (Simp_tac 1);
  24.129 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.130 +by (ALLGOALS Asm_full_simp_tac);
  24.131  qed "takeWhile_dropWhile_id";
  24.132  Addsimps [takeWhile_dropWhile_id];
  24.133  
  24.134  goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
  24.135  by (induct_tac "xs" 1);
  24.136 - by (Simp_tac 1);
  24.137 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.138 +by (ALLGOALS Asm_full_simp_tac);
  24.139  by (Blast_tac 1);
  24.140  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
  24.141  Addsimps [takeWhile_append1];
  24.142 @@ -767,16 +763,14 @@
  24.143  goal thy
  24.144    "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
  24.145  by (induct_tac "xs" 1);
  24.146 - by (Simp_tac 1);
  24.147 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.148 +by (ALLGOALS Asm_full_simp_tac);
  24.149  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
  24.150  Addsimps [takeWhile_append2];
  24.151  
  24.152  goal thy
  24.153    "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
  24.154  by (induct_tac "xs" 1);
  24.155 - by (Simp_tac 1);
  24.156 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.157 +by (ALLGOALS Asm_full_simp_tac);
  24.158  by (Blast_tac 1);
  24.159  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
  24.160  Addsimps [dropWhile_append1];
  24.161 @@ -784,15 +778,13 @@
  24.162  goal thy
  24.163    "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
  24.164  by (induct_tac "xs" 1);
  24.165 - by (Simp_tac 1);
  24.166 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.167 +by (ALLGOALS Asm_full_simp_tac);
  24.168  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
  24.169  Addsimps [dropWhile_append2];
  24.170  
  24.171  goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
  24.172  by (induct_tac "xs" 1);
  24.173 - by (Simp_tac 1);
  24.174 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.175 +by (ALLGOALS Asm_full_simp_tac);
  24.176  qed_spec_mp"set_take_whileD";
  24.177  
  24.178  qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
  24.179 @@ -805,21 +797,18 @@
  24.180  goal thy "set(remdups xs) = set xs";
  24.181  by (induct_tac "xs" 1);
  24.182   by (Simp_tac 1);
  24.183 -by (asm_full_simp_tac (simpset() addsimps [insert_absorb]
  24.184 -                                 addsplits [expand_if]) 1);
  24.185 +by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);
  24.186  qed "set_remdups";
  24.187  Addsimps [set_remdups];
  24.188  
  24.189  goal thy "nodups(remdups xs)";
  24.190  by (induct_tac "xs" 1);
  24.191 - by (Simp_tac 1);
  24.192 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.193 +by (ALLGOALS Asm_full_simp_tac);
  24.194  qed "nodups_remdups";
  24.195  
  24.196  goal thy "nodups xs --> nodups (filter P xs)";
  24.197  by (induct_tac "xs" 1);
  24.198 - by (Simp_tac 1);
  24.199 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  24.200 +by (ALLGOALS Asm_full_simp_tac);
  24.201  qed_spec_mp "nodups_filter";
  24.202  
  24.203  (** replicate **)
    25.1 --- a/src/HOL/Map.ML	Fri Mar 06 18:25:28 1998 +0100
    25.2 +++ b/src/HOL/Map.ML	Sat Mar 07 16:29:29 1998 +0100
    25.3 @@ -21,7 +21,7 @@
    25.4  qed_goal "update_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
    25.5  	(K [Asm_simp_tac 1]);
    25.6  qed_goal "update_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
    25.7 -	(K [rtac ext 1, asm_simp_tac (simpset() addsplits [expand_if]) 1]);
    25.8 +	(K [rtac ext 1, Asm_simp_tac 1]);
    25.9  (*Addsimps [update_same, update_other, update_triv];*)
   25.10  
   25.11  section "++";
   25.12 @@ -56,14 +56,14 @@
   25.13  by (induct_tac "xs" 1);
   25.14  by (Simp_tac 1);
   25.15  by (rtac ext 1);
   25.16 -by (asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
   25.17 +by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
   25.18  qed "map_of_append";
   25.19  Addsimps [map_of_append];
   25.20  
   25.21  goal thy "map_of xs k = Some y --> (k,y):set xs";
   25.22  by (list.induct_tac "xs" 1);
   25.23  by  (Simp_tac 1);
   25.24 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   25.25 +by (Asm_simp_tac 1);
   25.26  by (split_all_tac 1);
   25.27  by (Simp_tac 1);
   25.28  qed_spec_mp "map_of_SomeD";
   25.29 @@ -76,7 +76,7 @@
   25.30  Addsimps [dom_empty];
   25.31  
   25.32  goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
   25.33 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   25.34 +by (Simp_tac 1);
   25.35  by (Blast_tac 1);
   25.36  qed "dom_update";
   25.37  Addsimps [dom_update];
    26.1 --- a/src/HOL/MiniML/Generalize.ML	Fri Mar 06 18:25:28 1998 +0100
    26.2 +++ b/src/HOL/MiniML/Generalize.ML	Sat Mar 07 16:29:29 1998 +0100
    26.3 @@ -45,8 +45,8 @@
    26.4  by (typ.induct_tac "t1" 1);
    26.5  by (Simp_tac 1);
    26.6  by (case_tac "nat : free_tv A" 1);
    26.7 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    26.8 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    26.9 +by (Asm_simp_tac 1);
   26.10 +by (Asm_simp_tac 1);
   26.11  by (Fast_tac 1);
   26.12  by (Asm_simp_tac 1);
   26.13  by (Fast_tac 1);
   26.14 @@ -97,7 +97,7 @@
   26.15  by (rename_tac "R" 1);
   26.16  by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
   26.17  by (typ.induct_tac "t" 1);
   26.18 - by (simp_tac (simpset() addsplits [expand_if]) 1);
   26.19 + by (Simp_tac 1);
   26.20  by (Asm_simp_tac 1);
   26.21  qed "gen_bound_typ_instance";
   26.22  
   26.23 @@ -107,7 +107,7 @@
   26.24  by (rename_tac "S" 1);
   26.25  by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
   26.26  by (typ.induct_tac "t" 1);
   26.27 - by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   26.28 + by (Asm_simp_tac 1);
   26.29   by (Fast_tac 1);
   26.30  by (Asm_simp_tac 1);
   26.31  qed "free_tv_subset_gen_le";
   26.32 @@ -121,8 +121,8 @@
   26.33  by (typ.induct_tac "t" 1);
   26.34  by (Simp_tac 1);
   26.35  by (case_tac "nat : free_tv A" 1);
   26.36 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   26.37 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   26.38 +by (Asm_simp_tac 1);
   26.39 +by (Asm_simp_tac 1);
   26.40  by (subgoal_tac "n <= n + nat" 1);
   26.41  by (forw_inst_tac [("t","A")] new_tv_le 1);
   26.42  by (assume_tac 1);
    27.1 --- a/src/HOL/MiniML/Instance.ML	Fri Mar 06 18:25:28 1998 +0100
    27.2 +++ b/src/HOL/MiniML/Instance.ML	Sat Mar 07 16:29:29 1998 +0100
    27.3 @@ -66,8 +66,8 @@
    27.4  by (rename_tac "S1 S2" 1);
    27.5  by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
    27.6  by Safe_tac;
    27.7 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    27.8 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    27.9 +by (Asm_simp_tac 1);
   27.10 +by (Asm_simp_tac 1);
   27.11  by (strip_tac 1);
   27.12  by (dres_inst_tac [("x","x")] bspec 1);
   27.13  by (assume_tac 1);
   27.14 @@ -82,8 +82,8 @@
   27.15  goal thy "!!sch. new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
   27.16  \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
   27.17  by (type_scheme.induct_tac "sch" 1);
   27.18 -by (simp_tac (simpset() addsimps [leD] addsplits [expand_if]) 1);
   27.19 -by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2] addsplits [expand_if]) 1);
   27.20 +by (simp_tac (simpset() addsimps [leD]) 1);
   27.21 +by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
   27.22  by (Asm_simp_tac 1);
   27.23  qed_spec_mp "subst_to_scheme_inverse";
   27.24  
   27.25 @@ -96,9 +96,9 @@
   27.26  \        (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
   27.27  \                         bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch)";
   27.28  by (type_scheme.induct_tac "sch" 1);
   27.29 -by (simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
   27.30 +by (simp_tac (simpset() addsimps [leD]) 1);
   27.31  by (Asm_simp_tac 1);
   27.32 -by (asm_full_simp_tac (simpset() addsplits [expand_if] addsimps [leD]) 1);
   27.33 +by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
   27.34  val aux2 = result () RS mp;
   27.35  
   27.36  
    28.1 --- a/src/HOL/MiniML/MiniML.ML	Fri Mar 06 18:25:28 1998 +0100
    28.2 +++ b/src/HOL/MiniML/MiniML.ML	Sat Mar 07 16:29:29 1998 +0100
    28.3 @@ -82,7 +82,7 @@
    28.4  goalw thy [free_tv_subst,dom_def]
    28.5            "!!A. dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
    28.6  \               free_tv A Un free_tv t";
    28.7 -by (simp_tac (simpset() addsplits [expand_if]) 1);
    28.8 +by (Simp_tac 1);
    28.9  by (Fast_tac 1);
   28.10  qed "dom_S'";
   28.11  
   28.12 @@ -110,7 +110,7 @@
   28.13  \         (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
   28.14  \         {x. ? y. x = n + y}";
   28.15  by (typ.induct_tac "t1" 1);
   28.16 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   28.17 +by (Simp_tac 1);
   28.18  by (Fast_tac 1);
   28.19  by (Simp_tac 1);
   28.20  by (Fast_tac 1);
    29.1 --- a/src/HOL/MiniML/Type.ML	Fri Mar 06 18:25:28 1998 +0100
    29.2 +++ b/src/HOL/MiniML/Type.ML	Sat Mar 07 16:29:29 1998 +0100
    29.3 @@ -352,7 +352,7 @@
    29.4  
    29.5  goal thy "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
    29.6  by (type_scheme.induct_tac "sch" 1);
    29.7 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    29.8 +by (ALLGOALS Asm_simp_tac);
    29.9  by (strip_tac 1);
   29.10  by (Fast_tac 1);
   29.11  qed "free_tv_ML_scheme";
   29.12 @@ -423,14 +423,14 @@
   29.13  goal thy
   29.14    "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
   29.15  by (typ.induct_tac "t" 1);
   29.16 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   29.17 +by (ALLGOALS Asm_simp_tac);
   29.18  qed "subst_te_new_tv";
   29.19  Addsimps [subst_te_new_tv];
   29.20  
   29.21  goal thy
   29.22    "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
   29.23  by (type_scheme.induct_tac "sch" 1);
   29.24 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   29.25 +by (ALLGOALS Asm_simp_tac);
   29.26  qed_spec_mp "subst_te_new_type_scheme";
   29.27  Addsimps [subst_te_new_type_scheme];
   29.28  
   29.29 @@ -547,13 +547,13 @@
   29.30  Addsimps [new_tv_not_free_tv];
   29.31  
   29.32  goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
   29.33 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   29.34 +by (Simp_tac 1);
   29.35  by Safe_tac;
   29.36  by (trans_tac 1);
   29.37  qed "less_maxL";
   29.38  
   29.39  goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
   29.40 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   29.41 +by (Simp_tac 1);
   29.42  by (fast_tac (claset() addDs [not_leE] addIs [less_trans]) 1);
   29.43  val less_maxR = result();
   29.44  
   29.45 @@ -586,11 +586,11 @@
   29.46  Addsimps [fresh_variable_type_schemes];
   29.47  
   29.48  goalw thy [max_def] "!!n::nat. n <= (max n n')";
   29.49 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   29.50 +by (Simp_tac 1);
   29.51  val le_maxL = result();
   29.52  
   29.53  goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
   29.54 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   29.55 +by (Simp_tac 1);
   29.56  by (fast_tac (claset() addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
   29.57  val le_maxR = result();
   29.58  
    30.1 --- a/src/HOL/MiniML/W.ML	Fri Mar 06 18:25:28 1998 +0100
    30.2 +++ b/src/HOL/MiniML/W.ML	Sat Mar 07 16:29:29 1998 +0100
    30.3 @@ -18,7 +18,7 @@
    30.4          "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
    30.5  by (expr.induct_tac "e" 1);
    30.6  (* case Var(n) *)
    30.7 -by (simp_tac (simpset() addsplits [split_option_bind,expand_if]) 1);
    30.8 +by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    30.9  (* case Abs e *)
   30.10  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   30.11  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   30.12 @@ -58,7 +58,7 @@
   30.13  by (assume_tac 2);
   30.14  by (rtac add_le_mono 1);
   30.15  by (Simp_tac 1);
   30.16 -by (simp_tac (simpset() addsplits [expand_if] addsimps [max_def]) 1);
   30.17 +by (simp_tac (simpset() addsimps [max_def]) 1);
   30.18  by (strip_tac 1);
   30.19  by (rtac new_tv_le 1);
   30.20  by (mp_tac 2);
   30.21 @@ -66,7 +66,7 @@
   30.22  by (assume_tac 2);
   30.23  by (rtac add_le_mono 1);
   30.24  by (Simp_tac 1);
   30.25 -by (simp_tac (simpset() addsplits [expand_if] addsimps [max_def]) 1);
   30.26 +by (simp_tac (simpset() addsimps [max_def]) 1);
   30.27  by (strip_tac 1);
   30.28  by (dtac not_leE 1);
   30.29  by (rtac less_or_eq_imp_le 1);
   30.30 @@ -81,7 +81,7 @@
   30.31  \                 new_tv m S & new_tv m t";
   30.32  by (expr.induct_tac "e" 1);
   30.33  (* case Var n *)
   30.34 -by (simp_tac (simpset() addsplits [split_option_bind,expand_if]) 1);
   30.35 +by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   30.36  by (strip_tac 1);
   30.37  by (dtac new_tv_nth_nat_A 1);
   30.38  by (assume_tac 1);
   30.39 @@ -178,7 +178,7 @@
   30.40  by (expr.induct_tac "e" 1);
   30.41  (* case Var n *)
   30.42  by (simp_tac (simpset() addsimps
   30.43 -    [free_tv_subst] addsplits [split_option_bind,expand_if]) 1);
   30.44 +    [free_tv_subst] addsplits [split_option_bind]) 1);
   30.45  by (strip_tac 1);
   30.46  by (case_tac "v : free_tv (A!nat)" 1);
   30.47  by (Asm_full_simp_tac 1);
   30.48 @@ -272,7 +272,7 @@
   30.49          "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
   30.50  by (expr.induct_tac "e" 1);
   30.51  (* case Var n *)
   30.52 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   30.53 +by (Asm_full_simp_tac 1);
   30.54  by (strip_tac 1);
   30.55  by (rtac has_type.VarI 1);
   30.56  by (Simp_tac 1);
   30.57 @@ -396,7 +396,7 @@
   30.58  by (expr.induct_tac "e" 1);
   30.59  (* case Var n *)
   30.60  by (strip_tac 1);
   30.61 -by (simp_tac (simpset() addcongs [conj_cong] addsplits [expand_if]) 1);
   30.62 +by (simp_tac (simpset() addcongs [conj_cong]) 1);
   30.63  by (eresolve_tac has_type_casesE 1); 
   30.64  by (asm_full_simp_tac (simpset() addsimps [is_bound_typ_instance]) 1);
   30.65  by (etac exE 1);
   30.66 @@ -457,7 +457,7 @@
   30.67  by (case_tac "na:free_tv Sa" 2);
   30.68  (* n1 ~: free_tv S1 *)
   30.69  by (forward_tac [not_free_impl_id] 3);
   30.70 -by (asm_simp_tac (simpset() addsplits [expand_if]) 3);
   30.71 +by (Asm_simp_tac 3);
   30.72  (* na : free_tv Sa *)
   30.73  by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
   30.74  by (dtac eq_subst_scheme_list_eq_free 2);
   30.75 @@ -465,7 +465,7 @@
   30.76  by (Asm_simp_tac 2); 
   30.77  by (case_tac "na:dom Sa" 2);
   30.78  (* na ~: dom Sa *)
   30.79 -by (asm_full_simp_tac (simpset() addsimps [dom_def] addsplits [expand_if]) 3);
   30.80 +by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
   30.81  (* na : dom Sa *)
   30.82  by (rtac eq_free_eq_subst_te 2);
   30.83  by (strip_tac 2);
   30.84 @@ -476,8 +476,7 @@
   30.85  by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3);
   30.86  by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
   30.87      (simpset() addsimps [cod_def,free_tv_subst])) 3);
   30.88 -by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst] 
   30.89 -                                     addsplits [expand_if])) 2);
   30.90 +by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
   30.91  by (Simp_tac 2);  
   30.92  by (rtac eq_free_eq_subst_te 2);
   30.93  by (strip_tac 2 );
   30.94 @@ -488,10 +487,10 @@
   30.95  by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3);
   30.96  by (case_tac "na: free_tv t - free_tv Sa" 2);
   30.97  (* case na ~: free_tv t - free_tv Sa *)
   30.98 -by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 3);
   30.99 +by (Asm_full_simp_tac 3);
  30.100  by (Fast_tac 3);
  30.101  (* case na : free_tv t - free_tv Sa *)
  30.102 -by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
  30.103 +by (Asm_full_simp_tac 2);
  30.104  by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2);
  30.105  by (dtac eq_subst_scheme_list_eq_free 2);
  30.106  by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
  30.107 @@ -527,9 +526,9 @@
  30.108      new_tv_not_free_tv]) 2);
  30.109  by (case_tac "na: free_tv t - free_tv Sa" 1);
  30.110  (* case na ~: free_tv t - free_tv Sa *)
  30.111 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
  30.112 +by (Asm_full_simp_tac 2);
  30.113  (* case na : free_tv t - free_tv Sa *)
  30.114 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
  30.115 +by (Asm_full_simp_tac 1);
  30.116  by (dtac (free_tv_app_subst_scheme_list RS subsetD) 1);
  30.117  by (fast_tac (set_cs addDs [codD,subst_comp_scheme_list RSN (2,trans),
  30.118      eq_subst_scheme_list_eq_free] addss ((simpset() addsimps 
    31.1 --- a/src/HOL/Nat.ML	Fri Mar 06 18:25:28 1998 +0100
    31.2 +++ b/src/HOL/Nat.ML	Sat Mar 07 16:29:29 1998 +0100
    31.3 @@ -15,7 +15,6 @@
    31.4  qed "min_0R";
    31.5  
    31.6  goalw thy [min_def] "min (Suc m) (Suc n) = Suc(min m n)";
    31.7 -by (split_tac [expand_if] 1);
    31.8  by (Simp_tac 1);
    31.9  qed "min_Suc_Suc";
   31.10  
    32.1 --- a/src/HOL/NatDef.ML	Fri Mar 06 18:25:28 1998 +0100
    32.2 +++ b/src/HOL/NatDef.ML	Sat Mar 07 16:29:29 1998 +0100
    32.3 @@ -599,12 +599,12 @@
    32.4  (** max
    32.5  
    32.6  goalw thy [max_def] "!!z::nat. (z <= max x y) = (z <= x | z <= y)";
    32.7 -by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
    32.8 +by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
    32.9  by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
   32.10  qed "le_max_iff_disj";
   32.11  
   32.12  goalw thy [max_def] "!!z::nat. (max x y <= z) = (x <= z & y <= z)";
   32.13 -by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
   32.14 +by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
   32.15  by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
   32.16  qed "max_le_iff_conj";
   32.17  
   32.18 @@ -612,12 +612,12 @@
   32.19  (** min **)
   32.20  
   32.21  goalw thy [min_def] "!!z::nat. (z <= min x y) = (z <= x & z <= y)";
   32.22 -by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
   32.23 +by (simp_tac (simpset() addsimps [not_le_iff_less]) 1);
   32.24  by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
   32.25  qed "le_min_iff_conj";
   32.26  
   32.27  goalw thy [min_def] "!!z::nat. (min x y <= z) = (x <= z | y <= z)";
   32.28 -by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits [expand_if]) 1);
   32.29 +by (simp_tac (simpset() addsimps [not_le_iff_less] addsplits) 1);
   32.30  by (blast_tac (claset() addIs [less_imp_le, le_trans]) 1);
   32.31  qed "min_le_iff_disj";
   32.32   **)
    33.1 --- a/src/HOL/Ord.ML	Fri Mar 06 18:25:28 1998 +0100
    33.2 +++ b/src/HOL/Ord.ML	Sat Mar 07 16:29:29 1998 +0100
    33.3 @@ -43,14 +43,12 @@
    33.4  (** min **)
    33.5  
    33.6  goalw thy [min_def] "!!least. (!!x. least <= x) ==> min least x = least";
    33.7 -by (split_tac [expand_if] 1);
    33.8  by (Asm_simp_tac 1);
    33.9  qed "min_leastL";
   33.10  
   33.11  val prems = goalw thy [min_def]
   33.12   "(!!x::'a::order. least <= x) ==> min x least = least";
   33.13  by (cut_facts_tac prems 1);
   33.14 -by (split_tac [expand_if] 1);
   33.15  by (Asm_simp_tac 1);
   33.16  by (blast_tac (claset() addIs [order_antisym]) 1);
   33.17  qed "min_leastR";
   33.18 @@ -65,25 +63,25 @@
   33.19  qed "linorder_less_linear";
   33.20  
   33.21  goalw thy [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
   33.22 -by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
   33.23 +by (Simp_tac 1);
   33.24  by(cut_facts_tac [linorder_linear] 1);
   33.25  by (blast_tac (claset() addIs [order_trans]) 1);
   33.26  qed "le_max_iff_disj";
   33.27  
   33.28  goalw thy [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
   33.29 -by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
   33.30 +by (Simp_tac 1);
   33.31  by(cut_facts_tac [linorder_linear] 1);
   33.32  by (blast_tac (claset() addIs [order_trans]) 1);
   33.33  qed "max_le_iff_conj";
   33.34  
   33.35  goalw thy [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
   33.36 -by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
   33.37 +by (Simp_tac 1);
   33.38  by(cut_facts_tac [linorder_linear] 1);
   33.39  by (blast_tac (claset() addIs [order_trans]) 1);
   33.40  qed "le_min_iff_conj";
   33.41  
   33.42  goalw thy [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
   33.43 -by (simp_tac (simpset() addsimps [] addsplits [expand_if]) 1);
   33.44 +by (Simp_tac 1);
   33.45  by(cut_facts_tac [linorder_linear] 1);
   33.46  by (blast_tac (claset() addIs [order_trans]) 1);
   33.47  qed "min_le_iff_disj";
    34.1 --- a/src/HOL/Set.ML	Fri Mar 06 18:25:28 1998 +0100
    34.2 +++ b/src/HOL/Set.ML	Sat Mar 07 16:29:29 1998 +0100
    34.3 @@ -664,7 +664,7 @@
    34.4  
    34.5  (*Not for Addsimps -- it can cause goals to blow up!*)
    34.6  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    34.7 -by (simp_tac (simpset() addsplits [expand_if]) 1);
    34.8 +by (Simp_tac 1);
    34.9  qed "mem_if";
   34.10  
   34.11  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    35.1 --- a/src/HOL/Subst/Subst.ML	Fri Mar 06 18:25:28 1998 +0100
    35.2 +++ b/src/HOL/Subst/Subst.ML	Sat Mar 07 16:29:29 1998 +0100
    35.3 @@ -41,7 +41,7 @@
    35.4  qed "agreement";
    35.5  
    35.6  goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
    35.7 -by (simp_tac (simpset() addsimps [agreement] addsplits [expand_if]) 1);
    35.8 +by (simp_tac (simpset() addsimps [agreement]) 1);
    35.9  qed_spec_mp"repl_invariance";
   35.10  
   35.11  val asms = goal Subst.thy 
   35.12 @@ -111,7 +111,7 @@
   35.13  by (induct_tac "t" 1);
   35.14  by (ALLGOALS Asm_simp_tac);
   35.15  by (alist_ind_tac "r" 1);
   35.16 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   35.17 +by (ALLGOALS Asm_simp_tac);
   35.18  qed "subst_comp";
   35.19  
   35.20  Addsimps [subst_comp];
   35.21 @@ -130,7 +130,7 @@
   35.22  by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
   35.23  by (rtac allI 1);
   35.24  by (induct_tac "t" 1);
   35.25 -by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [expand_if])));
   35.26 +by (ALLGOALS Asm_full_simp_tac);
   35.27  qed "Cons_trivial";
   35.28  
   35.29  
   35.30 @@ -143,7 +143,7 @@
   35.31  
   35.32  goal Subst.thy  "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
   35.33  by (alist_ind_tac "s" 1);
   35.34 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   35.35 +by (ALLGOALS Asm_simp_tac);
   35.36  by (Blast_tac 1);
   35.37  qed "sdom_iff";
   35.38  
   35.39 @@ -203,7 +203,7 @@
   35.40  
   35.41  goal Subst.thy "(M <| [(x, Var x)]) = M";
   35.42  by (induct_tac "M" 1);
   35.43 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   35.44 +by (ALLGOALS Asm_simp_tac);
   35.45  qed "id_subst_lemma";
   35.46  
   35.47  Addsimps [id_subst_lemma];
    36.1 --- a/src/HOL/Subst/Unifier.ML	Fri Mar 06 18:25:28 1998 +0100
    36.2 +++ b/src/HOL/Subst/Unifier.ML	Sat Mar 07 16:29:29 1998 +0100
    36.3 @@ -82,8 +82,7 @@
    36.4  
    36.5  goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
    36.6  by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
    36.7 -				 empty_iff_all_not]
    36.8 -                       addsplits [expand_if]) 1);
    36.9 +				 empty_iff_all_not]) 1);
   36.10  by (Blast_tac 1);
   36.11  qed_spec_mp "Var_Idem";
   36.12  
    37.1 --- a/src/HOL/Subst/Unify.ML	Fri Mar 06 18:25:28 1998 +0100
    37.2 +++ b/src/HOL/Subst/Unify.ML	Sat Mar 07 16:29:29 1998 +0100
    37.3 @@ -153,8 +153,7 @@
    37.4  (* Apply induction *)
    37.5  by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
    37.6  by (ALLGOALS 
    37.7 -    (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0)
    37.8 -			    addsplits [expand_if])));
    37.9 +    (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0))));
   37.10  (*Const-Const case*)
   37.11  by (simp_tac
   37.12      (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
   37.13 @@ -207,7 +206,7 @@
   37.14  
   37.15  goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
   37.16  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
   37.17 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   37.18 +by (ALLGOALS Asm_simp_tac);
   37.19  (*Const-Const case*)
   37.20  by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
   37.21  (*Const-Var case*)
   37.22 @@ -245,8 +244,7 @@
   37.23  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
   37.24  by (ALLGOALS 
   37.25      (asm_simp_tac 
   37.26 -       (simpset() addsimps [Var_Idem] 
   37.27 -	         addsplits [expand_if,split_option_case])));
   37.28 +       (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
   37.29  (*Comb-Comb case*)
   37.30  by Safe_tac;
   37.31  by (REPEAT (dtac spec 1 THEN mp_tac 1));
    38.1 --- a/src/HOL/W0/I.ML	Fri Mar 06 18:25:28 1998 +0100
    38.2 +++ b/src/HOL/W0/I.ML	Sat Mar 07 16:29:29 1998 +0100
    38.3 @@ -144,7 +144,7 @@
    38.4  goal I.thy "!a m s. \
    38.5  \  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
    38.6  by (expr.induct_tac "e" 1);
    38.7 -  by (simp_tac (simpset() addsimps [app_subst_list] addsplits [expand_if]) 1);
    38.8 +  by (simp_tac (simpset() addsimps [app_subst_list]) 1);
    38.9   by (Simp_tac 1);
   38.10   by (strip_tac 1);
   38.11   by (subgoal_tac "TVar m # $ s a = $s(TVar m # a)" 1);
    39.1 --- a/src/HOL/W0/Type.ML	Fri Mar 06 18:25:28 1998 +0100
    39.2 +++ b/src/HOL/W0/Type.ML	Sat Mar 07 16:29:29 1998 +0100
    39.3 @@ -157,7 +157,7 @@
    39.4  goal thy
    39.5    "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
    39.6  by (typ.induct_tac "t" 1);
    39.7 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
    39.8 +by (ALLGOALS Asm_simp_tac);
    39.9  qed "subst_te_new_tv";
   39.10  Addsimps [subst_te_new_tv];
   39.11  
   39.12 @@ -259,7 +259,7 @@
   39.13  (* case [] *)
   39.14  by (Simp_tac 1);
   39.15  (* case x#xl *)
   39.16 -by (fast_tac (set_cs addss(simpset() addsplits [expand_if])) 1);
   39.17 +by (fast_tac (set_cs addss simpset()) 1);
   39.18  qed_spec_mp "ftv_mem_sub_ftv_list";
   39.19  Addsimps [ftv_mem_sub_ftv_list];
   39.20  
    40.1 --- a/src/HOL/W0/W.ML	Fri Mar 06 18:25:28 1998 +0100
    40.2 +++ b/src/HOL/W0/W.ML	Sat Mar 07 16:29:29 1998 +0100
    40.3 @@ -14,7 +14,7 @@
    40.4          "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
    40.5  by (expr.induct_tac "e" 1);
    40.6  (* case Var n *)
    40.7 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    40.8 +by (Asm_simp_tac 1);
    40.9  (* case Abs e *)
   40.10  by (asm_full_simp_tac (simpset() addsimps [app_subst_list]
   40.11                          addsplits [expand_bind]) 1);
   40.12 @@ -45,7 +45,7 @@
   40.13          "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
   40.14  by (expr.induct_tac "e" 1);
   40.15  (* case Var(n) *)
   40.16 -by (fast_tac (HOL_cs addss(simpset() addsplits [expand_if])) 1);
   40.17 +by (fast_tac (HOL_cs addss simpset()) 1);
   40.18  (* case Abs e *)
   40.19  by (simp_tac (simpset() addsplits [expand_bind]) 1);
   40.20  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   40.21 @@ -91,8 +91,7 @@
   40.22  by (expr.induct_tac "e" 1);
   40.23  (* case Var n *)
   40.24  by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset() 
   40.25 -        addsimps [id_subst_def,new_tv_list,new_tv_subst] 
   40.26 -        addsplits [expand_if])) 1);
   40.27 +        addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
   40.28  (* case Abs e *)
   40.29  by (simp_tac (simpset() addsimps [new_tv_subst,new_tv_Suc_list] 
   40.30      addsplits [expand_bind]) 1);
   40.31 @@ -159,7 +158,7 @@
   40.32  by (expr.induct_tac "e" 1);
   40.33  (* case Var n *)
   40.34  by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
   40.35 -    addss (simpset() addsplits [expand_if])) 1);
   40.36 +    addss simpset()) 1);
   40.37  
   40.38  (* case Abs e *)
   40.39  by (asm_full_simp_tac (simpset() addsimps
   40.40 @@ -225,8 +224,7 @@
   40.41  by (expr.induct_tac "e" 1);
   40.42  (* case Var n *)
   40.43  by (strip_tac 1);
   40.44 -by (simp_tac (simpset() addcongs [conj_cong] 
   40.45 -              addsplits [expand_if]) 1);
   40.46 +by (simp_tac (simpset() addcongs [conj_cong]) 1);
   40.47  by (eresolve_tac has_type_casesE 1); 
   40.48  by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv,app_subst_list]) 1);
   40.49  by (res_inst_tac [("x","s'")] exI 1);
   40.50 @@ -284,7 +282,7 @@
   40.51  by (case_tac "na:free_tv sa" 2);
   40.52  (* na ~: free_tv sa *)
   40.53  by (forward_tac [not_free_impl_id] 3);
   40.54 -by (asm_simp_tac (simpset() addsplits [expand_if]) 3);
   40.55 +by (Asm_simp_tac 3);
   40.56  (* na : free_tv sa *)
   40.57  by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
   40.58  by (dtac eq_subst_tel_eq_free 2);
   40.59 @@ -293,8 +291,7 @@
   40.60  by (case_tac "na:dom sa" 2);
   40.61  (* na ~: dom sa *)
   40.62  (** LEVEL 50 **)
   40.63 -by (asm_full_simp_tac (simpset() addsimps [dom_def] 
   40.64 -                       addsplits [expand_if]) 3);
   40.65 +by (asm_full_simp_tac (simpset() addsimps [dom_def]) 3);
   40.66  (* na : dom sa *)
   40.67  by (rtac eq_free_eq_subst_te 2);
   40.68  by (strip_tac 2);
   40.69 @@ -305,8 +302,7 @@
   40.70  by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3);
   40.71  by (fast_tac (set_cs addDs [new_tv_W,new_tv_not_free_tv] addss 
   40.72                (simpset() addsimps [cod_def,free_tv_subst])) 3);
   40.73 -by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst] 
   40.74 -                            addsplits [expand_if])) 2);
   40.75 +by (fast_tac (set_cs addss (simpset() addsimps [cod_def,free_tv_subst])) 2);
   40.76  
   40.77  (** LEVEL 60 **)
   40.78  by (Simp_tac 2);  
   40.79 @@ -320,9 +316,9 @@
   40.80  by (case_tac "na: free_tv t - free_tv sa" 2);
   40.81  (** LEVEL 69 **)
   40.82  (* case na ~: free_tv t - free_tv sa *)
   40.83 -by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 3);
   40.84 +by (Asm_full_simp_tac 3);
   40.85  (* case na : free_tv t - free_tv sa *)
   40.86 -by ( asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
   40.87 +by (Asm_full_simp_tac 2);
   40.88  by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2);
   40.89  by (dtac eq_subst_tel_eq_free 2);
   40.90  by (fast_tac (HOL_cs addIs [free_tv_W,free_tv_le_new_tv] addDs [new_tv_W]) 2);
   40.91 @@ -358,9 +354,9 @@
   40.92      new_tv_not_free_tv]) 2);
   40.93  by (case_tac "na: free_tv t - free_tv sa" 1);
   40.94  (* case na ~: free_tv t - free_tv sa *)
   40.95 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 2);
   40.96 +by (Asm_full_simp_tac 2);
   40.97  (* case na : free_tv t - free_tv sa *)
   40.98 -by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);
   40.99 +by (Asm_full_simp_tac 1);
  40.100  by (dtac (free_tv_app_subst_tel RS subsetD) 1);
  40.101  by (fast_tac (set_cs addDs [codD,subst_comp_tel RSN (2,trans),
  40.102                              eq_subst_tel_eq_free] 
    41.1 --- a/src/HOL/WF.ML	Fri Mar 06 18:25:28 1998 +0100
    41.2 +++ b/src/HOL/WF.ML	Sat Mar 07 16:29:29 1998 +0100
    41.3 @@ -153,7 +153,7 @@
    41.4    H_cong to expose the equality*)
    41.5  goalw WF.thy [cut_def]
    41.6      "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
    41.7 -by (simp_tac (HOL_ss addsimps [expand_fun_eq] addsplits [expand_if]) 1);
    41.8 +by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
    41.9  qed "cuts_eq";
   41.10  
   41.11  goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
   41.12 @@ -193,8 +193,7 @@
   41.13  and fisg   = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal)));
   41.14  by (cut_facts_tac prems 1);
   41.15  by (rtac ext 1);
   41.16 -by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]
   41.17 -                              addsplits [expand_if]) 1);
   41.18 +by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1);
   41.19  qed "is_recfun_cut";
   41.20  
   41.21  (*** Main Existence Lemma -- Basic Properties of the_recfun ***)
    42.1 --- a/src/HOL/equalities.ML	Fri Mar 06 18:25:28 1998 +0100
    42.2 +++ b/src/HOL/equalities.ML	Sat Mar 07 16:29:29 1998 +0100
    42.3 @@ -115,7 +115,7 @@
    42.4  goalw thy [image_def]
    42.5  "(%x. if P x then f x else g x) `` S                    \
    42.6  \ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
    42.7 -by (split_tac [expand_if] 1);
    42.8 +by (Simp_tac 1);
    42.9  by (Blast_tac 1);
   42.10  qed "if_image_distrib";
   42.11  Addsimps[if_image_distrib];
   42.12 @@ -275,13 +275,13 @@
   42.13  
   42.14  goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
   42.15  \                                      else        B Int C)";
   42.16 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   42.17 +by (Simp_tac 1);
   42.18  by (Blast_tac 1);
   42.19  qed "Int_insert_left";
   42.20  
   42.21  goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
   42.22  \                                      else        A Int B)";
   42.23 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   42.24 +by (Simp_tac 1);
   42.25  by (Blast_tac 1);
   42.26  qed "Int_insert_right";
   42.27  
   42.28 @@ -612,7 +612,7 @@
   42.29  qed "Diff_insert2";
   42.30  
   42.31  goal thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
   42.32 -by (simp_tac (simpset() addsplits [expand_if]) 1);
   42.33 +by (Simp_tac 1);
   42.34  by (Blast_tac 1);
   42.35  qed "insert_Diff_if";
   42.36  
    43.1 --- a/src/HOL/ex/Fib.ML	Fri Mar 06 18:25:28 1998 +0100
    43.2 +++ b/src/HOL/ex/Fib.ML	Sat Mar 07 16:29:29 1998 +0100
    43.3 @@ -58,8 +58,7 @@
    43.4  by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
    43.5  by (ALLGOALS  (*using fib.rules here results in a longer proof!*)
    43.6      (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
    43.7 -				       mod_less, mod_Suc]
    43.8 -                             addsplits [expand_if])));
    43.9 +				       mod_less, mod_Suc])));
   43.10  by (ALLGOALS
   43.11      (asm_full_simp_tac
   43.12       (simpset() addsimps (fib.rules @ add_ac @ mult_ac @
    44.1 --- a/src/HOL/ex/InSort.ML	Fri Mar 06 18:25:28 1998 +0100
    44.2 +++ b/src/HOL/ex/InSort.ML	Sat Mar 07 16:29:29 1998 +0100
    44.3 @@ -8,8 +8,7 @@
    44.4  
    44.5  goal thy "!y. mset(ins f x xs) y = mset (x#xs) y";
    44.6  by (list.induct_tac "xs" 1);
    44.7 -by (Asm_simp_tac 1);
    44.8 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    44.9 +by (ALLGOALS Asm_simp_tac);
   44.10  qed "mset_ins";
   44.11  Addsimps [mset_ins];
   44.12  
   44.13 @@ -19,8 +18,7 @@
   44.14  qed "insort_permutes";
   44.15  
   44.16  goal thy "set(ins f x xs) = insert x (set xs)";
   44.17 -by (asm_simp_tac (simpset() addsimps [set_via_mset]
   44.18 -                           addsplits [expand_if]) 1);
   44.19 +by (asm_simp_tac (simpset() addsimps [set_via_mset]) 1);
   44.20  by (Fast_tac 1);
   44.21  qed "set_ins";
   44.22  Addsimps [set_ins];
   44.23 @@ -28,7 +26,7 @@
   44.24  val prems = goalw InSort.thy [total_def,transf_def]
   44.25    "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
   44.26  by (list.induct_tac "xs" 1);
   44.27 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   44.28 +by (ALLGOALS Asm_simp_tac);
   44.29  by (cut_facts_tac prems 1);
   44.30  by (Fast_tac 1);
   44.31  qed "sorted_ins";
    45.1 --- a/src/HOL/ex/Primes.ML	Fri Mar 06 18:25:28 1998 +0100
    45.2 +++ b/src/HOL/ex/Primes.ML	Sat Mar 07 16:29:29 1998 +0100
    45.3 @@ -36,7 +36,7 @@
    45.4  
    45.5  goal thy "!!m. 0<n ==> gcd(m,n) = gcd (n, m mod n)";
    45.6  by (rtac (gcd_eq RS trans) 1);
    45.7 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    45.8 +by (Asm_simp_tac 1);
    45.9  by (Blast_tac 1);
   45.10  qed "gcd_less_0";
   45.11  Addsimps [gcd_0, gcd_less_0];
    46.1 --- a/src/HOL/ex/Qsort.ML	Fri Mar 06 18:25:28 1998 +0100
    46.2 +++ b/src/HOL/ex/Qsort.ML	Sat Mar 07 16:29:29 1998 +0100
    46.3 @@ -26,7 +26,7 @@
    46.4  
    46.5  goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
    46.6  by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
    46.7 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
    46.8 +by (ALLGOALS Asm_simp_tac);
    46.9  qed "qsort_permutes";
   46.10  
   46.11  goal Qsort.thy "set(qsort le xs) = set xs";
   46.12 @@ -37,7 +37,7 @@
   46.13  goal List.thy
   46.14    "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
   46.15  by (list.induct_tac "xs" 1);
   46.16 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   46.17 +by (ALLGOALS Asm_simp_tac);
   46.18  qed"Ball_set_filter";
   46.19  Addsimps [Ball_set_filter];
   46.20  
    47.1 --- a/src/HOL/ex/Recdef.ML	Fri Mar 06 18:25:28 1998 +0100
    47.2 +++ b/src/HOL/ex/Recdef.ML	Sat Mar 07 16:29:29 1998 +0100
    47.3 @@ -13,7 +13,7 @@
    47.4  
    47.5  goal thy "(x mem qsort (ord,l)) = (x mem l)";
    47.6  by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
    47.7 -by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
    47.8 +by (ALLGOALS Asm_simp_tac);
    47.9  by (Blast_tac 1);
   47.10  qed "qsort_mem_stable";
   47.11  
    48.1 --- a/src/HOL/ex/Sorting.ML	Fri Mar 06 18:25:28 1998 +0100
    48.2 +++ b/src/HOL/ex/Sorting.ML	Sat Mar 07 16:29:29 1998 +0100
    48.3 @@ -8,20 +8,20 @@
    48.4  
    48.5  goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
    48.6  by (list.induct_tac "xs" 1);
    48.7 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
    48.8 +by (ALLGOALS Asm_simp_tac);
    48.9  qed "mset_append";
   48.10  
   48.11  goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
   48.12  \                     mset xs x";
   48.13  by (list.induct_tac "xs" 1);
   48.14 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   48.15 +by (ALLGOALS Asm_simp_tac);
   48.16  qed "mset_compl_add";
   48.17  
   48.18  Addsimps [mset_append, mset_compl_add];
   48.19  
   48.20  goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
   48.21  by (list.induct_tac "xs" 1);
   48.22 -by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
   48.23 +by (ALLGOALS Asm_simp_tac);
   48.24  by (Fast_tac 1);
   48.25  qed "set_via_mset";
   48.26  
    49.1 --- a/src/HOL/ex/set.ML	Fri Mar 06 18:25:28 1998 +0100
    49.2 +++ b/src/HOL/ex/set.ML	Sat Mar 07 16:29:29 1998 +0100
    49.3 @@ -81,7 +81,7 @@
    49.4  
    49.5  goalw Lfp.thy [image_def]
    49.6      "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)";
    49.7 -by (simp_tac (simpset() addsplits [expand_if]) 1);
    49.8 +by (Simp_tac 1);
    49.9  by (Blast_tac 1);
   49.10  qed "range_if_then_else";
   49.11