# HG changeset patch
# User nipkow
# Date 893688470 -7200
# Node ID 2e53109d4bc80d5f3249522f84d78e5b51f60938
# Parent  bc11b5b06f87c72763b75c84ac24547c7432b4ab
Renamed expand_const -> split_const

diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Fix.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -697,7 +697,7 @@
   "!!Q. chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)"
  (fn _ =>
         [
-        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
+        Asm_simp_tac 1,
         safe_tac HOL_cs,
         subgoal_tac "ia = i" 1,
         Asm_simp_tac 1,
@@ -708,7 +708,7 @@
   "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
  (fn _ =>
         [
-        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
+        Asm_simp_tac 1,
         strip_tac 1,
         etac allE 1,
         etac mp 1,
@@ -722,7 +722,7 @@
         [
         safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
         atac 2,
-        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
+        Asm_simp_tac 1,
         res_inst_tac [("x","i")] exI 1,
         strip_tac 1,
         trans_tac 1
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -18,7 +18,7 @@
 
 goalw thy [dlift_def]
  "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
-by (simp_tac (simpset() setloop (split_tac[expand_lift_case])) 1);
+by (simp_tac (simpset() addsplits [split_lift_case]) 1);
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
@@ -33,13 +33,13 @@
     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
- by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
+ by (Simp_tac 1);
  by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1);
 by (Simp_tac 1);
 by (rtac fix_ind 1);
   by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
  by (Simp_tac 1);
-by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
+by (Simp_tac 1);
 by (safe_tac HOL_cs);
   by (fast_tac (HOL_cs addIs evalc.intrs) 1);
  by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IMP/HoareEx.ML
--- a/src/HOLCF/IMP/HoareEx.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IMP/HoareEx.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -14,6 +14,6 @@
   (* simplifier with enhanced adm-tactic: *)
   by (Simp_tac 1);
  by (Simp_tac 1);
-by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "WHILE_rule_sound";
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/ABP/Correctness.ML
--- a/src/HOLCF/IOA/ABP/Correctness.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -54,7 +54,7 @@
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
  by (hyp_subst_tac 1);
- by (stac expand_if 1);
+ by (stac split_if 1);
  by (Asm_full_simp_tac 1);
  by (Asm_full_simp_tac 1);
 val l_iff_red_nil = result();
@@ -72,7 +72,7 @@
 by (asm_full_simp_tac list_ss 1);
 by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
-by (stac expand_if 1);
+by (stac split_if 1);
 by (REPEAT(hyp_subst_tac 1));
 by (etac subst 1);
 by (Simp_tac 1);
@@ -91,7 +91,7 @@
 by (Asm_full_simp_tac 1);
 by (REPEAT (etac exE 1));
 by (Asm_simp_tac 1);
-by (stac expand_if 1);
+by (stac split_if 1);
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1); 
 qed"rev_red_not_nil";
@@ -104,7 +104,7 @@
  by (asm_full_simp_tac list_ss 1);
  by (REPEAT (rtac allI 1)); 
  by (rtac impI 1); 
- by (stac expand_if 1);
+ by (stac split_if 1);
  by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
                           (rev_red_not_nil RS mp)])  1);
 qed"last_ind_on_first";
@@ -116,7 +116,7 @@
    "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then   \
 \      reduce(l@[x])=reduce(l) else                  \
 \      reduce(l@[x])=reduce(l)@[x]"; 
-by (stac expand_if 1);
+by (stac split_if 1);
 by (rtac conjI 1);
 (* --> *)
 by (List.list.induct_tac "l" 1);
@@ -136,11 +136,11 @@
 by (Simp_tac 1);
 by (case_tac "list=[]" 1);
 by (cut_inst_tac [("l","list")] cons_not_nil 2);
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (auto_tac (claset(), 
 	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
-                      setloop split_tac [expand_if]));
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+                      setloop split_tac [split_if]));
+by (Asm_full_simp_tac 1);
 qed"reduce_hd";
 
 
@@ -154,7 +154,7 @@
 by (Asm_full_simp_tac 1);
 by (REPEAT (etac exE 1));
 by (Asm_full_simp_tac 1);
-by (stac expand_if 1);
+by (stac split_if 1);
 by (rtac conjI 1);
 by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
 by (Step_tac 1);
@@ -167,7 +167,7 @@
           C h a n n e l   A b s t r a c t i o n
  *******************************************************************)
 
-Delsplits [expand_if];
+Delsplits [split_if];
 goal Correctness.thy 
       "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
 by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
@@ -221,7 +221,7 @@
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)
-by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
+by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"sender_unchanged";
 
 (* 2 copies of before *)
@@ -237,7 +237,7 @@
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)
-by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"receiver_unchanged";
 
 goal Correctness.thy 
@@ -252,9 +252,9 @@
 by (rtac imp_conj_lemma 1);
 by (Action.action.induct_tac "a" 1);
 (* 7 cases *)
-by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
 qed"env_unchanged";
-Addsplits [expand_if];
+Addsplits [split_if];
 
 goal Correctness.thy "compatible srch_ioa rsch_ioa"; 
 by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/ABP/Lemmas.ML
--- a/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -16,7 +16,7 @@
 val and_de_morgan_and_absorbe = result();
 
 goal HOL.thy "(if C then A else B) --> (A|B)";
-by (stac expand_if 1);
+by (stac split_if 1);
 by (Fast_tac 1);
 val bool_if_impl_or = result();
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/NTP/Correctness.ML
--- a/src/HOLCF/IOA/NTP/Correctness.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -68,7 +68,7 @@
 (* Proof of correctness *)
 goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
   "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by (simp_tac (simpset() delsplits [expand_if] addsimps 
+by (simp_tac (simpset() delsplits [split_if] addsimps 
     [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
 by (rtac conjI 1);
  by (simp_tac ss' 1);
@@ -77,7 +77,7 @@
 by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
 
 by (Action.action.induct_tac "a"  1);
-by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
+by (asm_simp_tac (ss' addsplits [split_if]) 1);
 by (forward_tac [inv4] 1);
 by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
 by (simp_tac ss' 1);
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/NTP/Impl.ML
--- a/src/HOLCF/IOA/NTP/Impl.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -60,12 +60,8 @@
                    addsimps transitions);     
 val rename_ss = (ss addsimps unfold_renaming);
 
-
-
-val tac     = asm_simp_tac ((ss addcongs [conj_cong]) 
-                            setloop (split_tac [expand_if]));
-val tac_ren = asm_simp_tac ((rename_ss addcongs [conj_cong]) 
-                            setloop (split_tac [expand_if]));
+val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]);
+val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]);
 
 
 
@@ -85,7 +81,7 @@
 
 (* First half *)
 by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
-                                 delsplits [expand_if]) 1);
+                                 delsplits [split_if]) 1);
 by (rtac Action.action.induct 1);
 
 by (EVERY1[tac, tac, tac, tac]);
@@ -103,7 +99,7 @@
 
 (* Now the other half *)
 by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
-                                 delsplits [expand_if]) 1);
+                                 delsplits [split_if]) 1);
 by (rtac Action.action.induct 1);
 by (EVERY1[tac, tac]);
 
@@ -114,7 +110,7 @@
 by (REPEAT (etac conjE 1));
 by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
                                       Multiset.countm_nonempty_def]
-                            addsplits [expand_if]) 1);
+                            addsplits [split_if]) 1);
 (* detour 2 *)
 by (tac 1);
 by (tac_ren 1);
@@ -124,7 +120,7 @@
                                          Multiset.count_def,
                                          Multiset.countm_nonempty_def,
                                          Multiset.delm_nonempty_def]
-                                 addsplits [expand_if]) 1);
+                                 addsplits [split_if]) 1);
 by (rtac allI 1);
 by (rtac conjI 1);
 by (rtac impI 1);
@@ -163,7 +159,7 @@
                            @ sender_projections @ impl_ioas)))
       1);
 
-  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
+  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
   by (Action.action.induct_tac "a" 1);
 
   (* 10 cases. First 4 are simple, since state doesn't change *)
@@ -224,11 +220,10 @@
                     (Impl.inv3_def :: (receiver_projections 
                                        @ sender_projections @ impl_ioas))) 1);
 
-  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
+  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
   by (Action.action.induct_tac "a" 1);
 
-val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] 
-                              setloop (split_tac [expand_if]));
+val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] addsplits [split_if]);
 
   (* 10 - 8 *)
 
@@ -291,11 +286,11 @@
                     (Impl.inv4_def :: (receiver_projections 
                                        @ sender_projections @ impl_ioas))) 1);
 
-  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
+  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
   by (Action.action.induct_tac "a" 1);
 
 val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]
-                              setloop (split_tac [expand_if]));
+                              setloop (split_tac [split_if]));
 
   (* 10 - 2 *)
   
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -36,7 +36,7 @@
 (* Arithmetic *)
 
 goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
-by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
+by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
 by (Blast_tac 1);
 qed "pred_suc";
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/NTP/Multiset.ML
--- a/src/HOLCF/IOA/NTP/Multiset.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -15,27 +15,23 @@
 goal Multiset.thy 
      "count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
   by (asm_simp_tac (simpset() addsimps 
-                    [Multiset.count_def,Multiset.countm_nonempty_def]
-                    setloop (split_tac [expand_if])) 1);
+                    [Multiset.count_def,Multiset.countm_nonempty_def]) 1);
 qed "count_addm_simp";
 
 goal Multiset.thy "count M y <= count (addm M x) y";
-  by (simp_tac (simpset() addsimps [count_addm_simp]
-                         setloop (split_tac [expand_if])) 1);
+  by (simp_tac (simpset() addsimps [count_addm_simp]) 1);
 qed "count_leq_addm";
 
 goalw Multiset.thy [Multiset.count_def] 
      "count (delm M x) y = (if y=x then count M y - 1 else count M y)";
-  by (res_inst_tac [("M","M")] Multiset.induction 1);
-  by (asm_simp_tac (simpset() 
-                   addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]
-                   setloop (split_tac [expand_if])) 1);
-  by (asm_full_simp_tac (simpset() 
+by (res_inst_tac [("M","M")] Multiset.induction 1);
+by (asm_simp_tac (simpset() 
+             addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1);
+by (asm_full_simp_tac (simpset() 
                          addsimps [Multiset.delm_nonempty_def,
-                                   Multiset.countm_nonempty_def]
-                         setloop (split_tac [expand_if])) 1);
-  by Safe_tac;
-  by (Asm_full_simp_tac 1);
+                                   Multiset.countm_nonempty_def]) 1);
+by Safe_tac;
+by (Asm_full_simp_tac 1);
 qed "count_delm_simp";
 
 goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
@@ -50,8 +46,7 @@
   by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
                                    Multiset.countm_empty_def]) 1);
   by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
-                                      Multiset.delm_nonempty_def]
-                             setloop (split_tac [expand_if])) 1);
+                                      Multiset.delm_nonempty_def]) 1);
 qed "countm_spurious_delm";
 
 
@@ -62,8 +57,7 @@
                            Multiset.countm_empty_def]) 1);
   by (asm_simp_tac (simpset() addsimps 
                        [Multiset.count_def,Multiset.delm_nonempty_def,
-                        Multiset.countm_nonempty_def]
-                    setloop (split_tac [expand_if])) 1);
+                        Multiset.countm_nonempty_def]) 1);
 qed_spec_mp "pos_count_imp_pos_countm";
 
 goal Multiset.thy
@@ -74,8 +68,7 @@
                            Multiset.countm_empty_def]) 1);
   by (asm_simp_tac (simpset() addsimps 
                       [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
-                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]
-                    addsplits [expand_if]) 1);
+                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
 qed "countm_done_delm";
 
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/Abstraction.ML
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -511,7 +511,7 @@
 temp_sat_def, satisfies_def,Next_def]
 "!! h. [| temp_strengthening P Q h |]\
 \      ==> temp_strengthening (Next P) (Next Q) h";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (safe_tac set_cs);
 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -393,8 +393,7 @@
 \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
 
   by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
-                            ioa_projections)
-                  setloop (split_tac [expand_if])) 1);
+                            ioa_projections)) 1);
 qed "trans_of_par4";
 
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -132,8 +132,7 @@
 
 goal thy "stutter sig (s, (a,t)>>ex) = \
 \     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
-by (simp_tac (simpset() addsimps [stutter_def] 
-                       setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [stutter_def]) 1);
 qed"stutter_cons";
 
 (* ----------------------------------------------------------------------------------- *)
@@ -167,8 +166,7 @@
 (* main case *)
 ren "ss a t" 1;
 by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
-                       setloop (split_tac [expand_if])) 1));
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
 qed"lemma_1_1a";
 
 
@@ -183,8 +181,7 @@
 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
 (* main case *)
 by (safe_tac set_cs);
-by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
-                 setloop (split_tac [expand_if])) 1));
+by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
 qed"lemma_1_1b";
 
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -112,8 +112,7 @@
 goal thy "!!x.[| x:act A; x~:act B |] \
 \   ==> mkex A B (x>>sch) (s,a>>exA) (t,exB)  =  \
 \       ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
-by (simp_tac (simpset() addsimps [mkex_def] 
-                       setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
 by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
 by Auto_tac;
 qed"mkex_cons_1";
@@ -121,8 +120,7 @@
 goal thy "!!x.[| x~:act A; x:act B |] \
 \   ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =  \ 
 \       ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
-by (simp_tac (simpset() addsimps [mkex_def] 
-                       setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
 by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
 by Auto_tac;
 qed"mkex_cons_2";
@@ -130,8 +128,7 @@
 goal thy "!!x.[| x:act A; x:act B |]  \
 \   ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
 \        ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
-by (simp_tac (simpset() addsimps [mkex_def] 
-                       setloop (split_tac [expand_if]) ) 1);
+by (simp_tac (simpset() addsimps [mkex_def]) 1);
 by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
 by Auto_tac;
 qed"mkex_cons_3";
@@ -216,7 +213,7 @@
 
 (* main case *) 
 (* splitting into 4 cases according to a:A, a:B *)
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (safe_tac set_cs);
 
 (* Case y:A, y:B *)
@@ -249,7 +246,7 @@
 
 fun mkex_induct_tac sch exA exB = 
     EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], 
-           asm_full_simp_tac (simpset() setloop split_tac [expand_if]),
+           Asm_full_simp_tac,
            SELECT_GOAL (safe_tac set_cs),
            Seq_case_simp_tac exA,
            Seq_case_simp_tac exB,
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -209,7 +209,7 @@
 by (etac Seq_Finite_ind  1);
 by (Asm_full_simp_tac 1);
 (* main case *)
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (safe_tac set_cs);
 
 (* a: act A; a: act B *)
@@ -479,7 +479,7 @@
 
 (* main case *) 
 (* splitting into 4 cases according to a:A, a:B *)
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (safe_tac set_cs);
 
 (* Case a:A, a:B *)
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -50,7 +50,7 @@
     Needs compositionality on schedule level, input-enabledness, compatibility
                     and distributivity of is_exec_frag over @@
 **********************************************************************************)
-Delsplits [expand_if];
+Delsplits [split_if];
 goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
 \            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
 \          ==> (sch @@ a>>nil) : schedules (A||B)";
@@ -83,7 +83,7 @@
 by (REPEAT (atac 1));
 qed"IOA_deadlock_free";
 
-Addsplits [expand_if];
+Addsplits [split_if];
 
 
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -129,7 +129,7 @@
 (* ------------------------------------------------------
                  Lemma 1 :Traces coincide  
    ------------------------------------------------------- *)
-Delsplits[expand_if];
+Delsplits[split_if];
 goalw thy [corresp_ex_def]
   "!!f.[|is_ref_map f C A; ext C = ext A|] ==>  \     
 \        !s. reachable C s & is_exec_frag C (s,xs) --> \
@@ -144,9 +144,9 @@
 by (eres_inst_tac [("x","y")] allE 1);
 by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [move_subprop4] 
-                          setloop split_tac [expand_if] ) 1);
+                          addsplits [split_if]) 1);
 qed"lemma_1";
-Addsplits[expand_if];
+Addsplits[split_if];
 
 (* ------------------------------------------------------------------ *)
 (*                   The following lemmata contribute to              *)
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -68,7 +68,7 @@
   by (fast_tac (claset() addDs prems) 1);
 val lemma = result();
 
-Delsplits [expand_if];
+Delsplits [split_if];
 goal thy "!!f.[| is_weak_ref_map f C A |]\
 \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
 by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
@@ -82,7 +82,7 @@
 by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,
 asig_outputs_def,asig_of_def,trans_of_def]) 1);
 by Safe_tac;
-by (stac expand_if 1);
+by (stac split_if 1);
  by (rtac conjI 1);
  by (rtac impI 1);
  by (etac disjE 1);
@@ -111,6 +111,6 @@
 by (forward_tac  [reachable_rename] 1);
 by Auto_tac;
 qed"rename_through_pmap";
-Addsplits [expand_if];
+Addsplits [split_if];
 
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -120,7 +120,7 @@
 goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
 by (simp_tac (simpset() addsimps [Last_def, Cons_def]) 1);
 by (res_inst_tac [("x","xs")] seq.casedist 1);
-by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_simp_tac 1);
 by (REPEAT (Asm_simp_tac 1));
 qed"Last_cons";
 
@@ -699,7 +699,7 @@
 by (Simp_tac 1);
 by (Simp_tac 1);
 (* main case *)
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
+by (Asm_full_simp_tac 1);
 qed"FilternPnilForallP1";
 
 bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
@@ -1158,8 +1158,7 @@
 (* FIX: better support for A = %x. True *)
 by (Fast_tac 3);
 by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
-by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3] 
-                                setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1);
 qed"FilterPQ_takelemma";
 
 Addsimps [FilterPQ];
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -156,7 +156,7 @@
                  Lemma 1 :Traces coincide  
    ------------------------------------------------------- *)
 
-Delsplits[expand_if];
+Delsplits[split_if];
 goal thy 
   "!!f.[|is_simulation R C A; ext C = ext A|] ==>  \     
 \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
@@ -177,9 +177,9 @@
 by (asm_full_simp_tac (simpset() addsimps 
       [rewrite_rule [Let_def] move_subprop5_sim,
        rewrite_rule [Let_def] move_subprop4_sim] 
-   setloop split_tac [expand_if] ) 1);
+   addsplits [split_if]) 1);
 qed_spec_mp"traces_coincide_sim";
-Addsplits[expand_if];
+Addsplits[split_if];
 
 
 (* ----------------------------------------------------------- *)
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/TL.ML
--- a/src/HOLCF/IOA/meta_theory/TL.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -138,7 +138,7 @@
 
 val tsuffix_TL2 = conjI RS tsuffix_TL;
 
-Delsplits[expand_if];
+Delsplits[split_if];
 goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
    "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
 auto();
@@ -146,33 +146,33 @@
 by (eres_inst_tac [("x","s")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
 (* []F .--> Next [] F *)
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
 auto();
 bd tsuffix_TL2 1;
 by (REPEAT (atac 1));
 auto();
 qed"LTL1";
-Addsplits[expand_if];
+Addsplits[split_if];
 
 
 goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
     "s |= .~ (Next F) .--> (Next (.~ F))";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 qed"LTL2a";
 
 goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
     "s |= (Next (.~ F)) .--> (.~ (Next F))";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 qed"LTL2b";
 
 goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
 "ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 qed"LTL3";
 
 goalw thy [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
  "s |= [] (F .--> Next F) .--> F .--> []F";
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 auto();
 
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/IOA/meta_theory/TLS.ML
--- a/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -84,7 +84,7 @@
 \  ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
 \             .--> (Next (Init (%(s,a,t).Q s))))";
 
-by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
+by (Asm_full_simp_tac 1);
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Lift3.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -94,12 +94,6 @@
 by (fast_tac (HOL_cs addSEs prems) 1);
 qed"Lift_cases";
 
-goal thy
-  "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
-by (lift.induct_tac "x" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "expand_lift_case";
-
 goal thy "(x~=UU)=(? y. x=Def y)";
 by (rtac iffI 1);
 by (rtac Lift_cases 1);
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/Sprod0.ML
--- a/src/HOLCF/Sprod0.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Sprod0.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -19,11 +19,11 @@
         (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl])
         ]);
 
-qed_goal "inj_onto_Abs_Sprod" Sprod0.thy 
-        "inj_onto Abs_Sprod Sprod"
+qed_goal "inj_on_Abs_Sprod" Sprod0.thy 
+        "inj_on Abs_Sprod Sprod"
 (fn prems =>
         [
-        (rtac inj_onto_inverseI 1),
+        (rtac inj_on_inverseI 1),
         (etac Abs_Sprod_inverse 1)
         ]);
 
@@ -80,7 +80,7 @@
         (cut_facts_tac prems 1),
         (etac inject_Spair_Rep 1),
         (atac 1),
-        (etac (inj_onto_Abs_Sprod  RS inj_ontoD) 1),
+        (etac (inj_on_Abs_Sprod  RS inj_onD) 1),
         (rtac SprodI 1),
         (rtac SprodI 1)
         ]);
@@ -132,7 +132,7 @@
         [
         (cut_facts_tac prems 1),
         (rtac defined_Spair_Rep_rev 1),
-        (rtac (inj_onto_Abs_Sprod  RS inj_ontoD) 1),
+        (rtac (inj_on_Abs_Sprod  RS inj_onD) 1),
         (atac 1),
         (rtac SprodI 1),
         (rtac SprodI 1)
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/Ssum0.ML
--- a/src/HOLCF/Ssum0.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Ssum0.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -30,10 +30,10 @@
         (rtac refl 1)
         ]);
 
-qed_goal "inj_onto_Abs_Ssum" Ssum0.thy "inj_onto Abs_Ssum Ssum"
+qed_goal "inj_on_Abs_Ssum" Ssum0.thy "inj_on Abs_Ssum Ssum"
 (fn prems =>
         [
-        (rtac inj_onto_inverseI 1),
+        (rtac inj_on_inverseI 1),
         (etac Abs_Ssum_inverse 1)
         ]);
 
@@ -89,7 +89,7 @@
         [
         (cut_facts_tac prems 1),
         (rtac noteq_SinlSinr_Rep 1),
-        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
+        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
         (rtac SsumIl 1),
         (rtac SsumIr 1)
         ]);
@@ -184,7 +184,7 @@
         [
         (cut_facts_tac prems 1),
         (rtac inject_Sinl_Rep 1),
-        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
+        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
         (rtac SsumIl 1),
         (rtac SsumIl 1)
         ]);
@@ -195,7 +195,7 @@
         [
         (cut_facts_tac prems 1),
         (rtac inject_Sinr_Rep 1),
-        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
+        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
         (rtac SsumIr 1),
         (rtac SsumIr 1)
         ]);
diff -r bc11b5b06f87 -r 2e53109d4bc8 src/HOLCF/Tr.ML
--- a/src/HOLCF/Tr.ML	Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/Tr.ML	Mon Apr 27 16:47:50 1998 +0200
@@ -99,10 +99,10 @@
   "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))";
 by (res_inst_tac [("p","Q")] trE 1);
 by (REPEAT (Asm_full_simp_tac 1));
-qed"expand_If2";
+qed"split_If2";
 
 val split_If_tac =
-  simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [expand_If2]);
+  simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [split_If2]);