Renamed expand_const -> split_const
authornipkow
Mon Apr 27 16:47:50 1998 +0200 (1998-04-27)
changeset 48332e53109d4bc8
parent 4832 bc11b5b06f87
child 4834 dd89afb55272
Renamed expand_const -> split_const
src/HOLCF/Fix.ML
src/HOLCF/IMP/Denotational.ML
src/HOLCF/IMP/HoareEx.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/NTP/Impl.ML
src/HOLCF/IOA/NTP/Lemmas.ML
src/HOLCF/IOA/NTP/Multiset.ML
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/SimCorrectness.ML
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/Lift3.ML
src/HOLCF/Sprod0.ML
src/HOLCF/Ssum0.ML
src/HOLCF/Tr.ML
     1.1 --- a/src/HOLCF/Fix.ML	Mon Apr 27 16:46:56 1998 +0200
     1.2 +++ b/src/HOLCF/Fix.ML	Mon Apr 27 16:47:50 1998 +0200
     1.3 @@ -697,7 +697,7 @@
     1.4    "!!Q. chain(Y) ==> chain(%m. if m < Suc i then Y(Suc i) else Y m)"
     1.5   (fn _ =>
     1.6          [
     1.7 -        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
     1.8 +        Asm_simp_tac 1,
     1.9          safe_tac HOL_cs,
    1.10          subgoal_tac "ia = i" 1,
    1.11          Asm_simp_tac 1,
    1.12 @@ -708,7 +708,7 @@
    1.13    "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
    1.14   (fn _ =>
    1.15          [
    1.16 -        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
    1.17 +        Asm_simp_tac 1,
    1.18          strip_tac 1,
    1.19          etac allE 1,
    1.20          etac mp 1,
    1.21 @@ -722,7 +722,7 @@
    1.22          [
    1.23          safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
    1.24          atac 2,
    1.25 -        asm_simp_tac (simpset() setloop (split_tac[expand_if])) 1,
    1.26 +        Asm_simp_tac 1,
    1.27          res_inst_tac [("x","i")] exI 1,
    1.28          strip_tac 1,
    1.29          trans_tac 1
     2.1 --- a/src/HOLCF/IMP/Denotational.ML	Mon Apr 27 16:46:56 1998 +0200
     2.2 +++ b/src/HOLCF/IMP/Denotational.ML	Mon Apr 27 16:47:50 1998 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4  
     2.5  goalw thy [dlift_def]
     2.6   "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
     2.7 -by (simp_tac (simpset() setloop (split_tac[expand_lift_case])) 1);
     2.8 +by (simp_tac (simpset() addsplits [split_lift_case]) 1);
     2.9  qed "dlift_is_Def";
    2.10  Addsimps [dlift_is_Def];
    2.11  
    2.12 @@ -33,13 +33,13 @@
    2.13      by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    2.14     by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    2.15    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
    2.16 - by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
    2.17 + by (Simp_tac 1);
    2.18   by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1);
    2.19  by (Simp_tac 1);
    2.20  by (rtac fix_ind 1);
    2.21    by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
    2.22   by (Simp_tac 1);
    2.23 -by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
    2.24 +by (Simp_tac 1);
    2.25  by (safe_tac HOL_cs);
    2.26    by (fast_tac (HOL_cs addIs evalc.intrs) 1);
    2.27   by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
     3.1 --- a/src/HOLCF/IMP/HoareEx.ML	Mon Apr 27 16:46:56 1998 +0200
     3.2 +++ b/src/HOLCF/IMP/HoareEx.ML	Mon Apr 27 16:47:50 1998 +0200
     3.3 @@ -14,6 +14,6 @@
     3.4    (* simplifier with enhanced adm-tactic: *)
     3.5    by (Simp_tac 1);
     3.6   by (Simp_tac 1);
     3.7 -by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
     3.8 +by (Simp_tac 1);
     3.9  by (Blast_tac 1);
    3.10  qed "WHILE_rule_sound";
     4.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Mon Apr 27 16:46:56 1998 +0200
     4.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Mon Apr 27 16:47:50 1998 +0200
     4.3 @@ -54,7 +54,7 @@
     4.4   by (REPEAT (rtac allI 1)); 
     4.5   by (rtac impI 1); 
     4.6   by (hyp_subst_tac 1);
     4.7 - by (stac expand_if 1);
     4.8 + by (stac split_if 1);
     4.9   by (Asm_full_simp_tac 1);
    4.10   by (Asm_full_simp_tac 1);
    4.11  val l_iff_red_nil = result();
    4.12 @@ -72,7 +72,7 @@
    4.13  by (asm_full_simp_tac list_ss 1);
    4.14  by (REPEAT (rtac allI 1)); 
    4.15   by (rtac impI 1); 
    4.16 -by (stac expand_if 1);
    4.17 +by (stac split_if 1);
    4.18  by (REPEAT(hyp_subst_tac 1));
    4.19  by (etac subst 1);
    4.20  by (Simp_tac 1);
    4.21 @@ -91,7 +91,7 @@
    4.22  by (Asm_full_simp_tac 1);
    4.23  by (REPEAT (etac exE 1));
    4.24  by (Asm_simp_tac 1);
    4.25 -by (stac expand_if 1);
    4.26 +by (stac split_if 1);
    4.27  by (hyp_subst_tac 1);
    4.28  by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1); 
    4.29  qed"rev_red_not_nil";
    4.30 @@ -104,7 +104,7 @@
    4.31   by (asm_full_simp_tac list_ss 1);
    4.32   by (REPEAT (rtac allI 1)); 
    4.33   by (rtac impI 1); 
    4.34 - by (stac expand_if 1);
    4.35 + by (stac split_if 1);
    4.36   by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
    4.37                            (rev_red_not_nil RS mp)])  1);
    4.38  qed"last_ind_on_first";
    4.39 @@ -116,7 +116,7 @@
    4.40     "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then   \
    4.41  \      reduce(l@[x])=reduce(l) else                  \
    4.42  \      reduce(l@[x])=reduce(l)@[x]"; 
    4.43 -by (stac expand_if 1);
    4.44 +by (stac split_if 1);
    4.45  by (rtac conjI 1);
    4.46  (* --> *)
    4.47  by (List.list.induct_tac "l" 1);
    4.48 @@ -136,11 +136,11 @@
    4.49  by (Simp_tac 1);
    4.50  by (case_tac "list=[]" 1);
    4.51  by (cut_inst_tac [("l","list")] cons_not_nil 2);
    4.52 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    4.53 +by (Asm_full_simp_tac 1);
    4.54  by (auto_tac (claset(), 
    4.55  	      impl_ss addsimps [last_ind_on_first,l_iff_red_nil] 
    4.56 -                      setloop split_tac [expand_if]));
    4.57 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    4.58 +                      setloop split_tac [split_if]));
    4.59 +by (Asm_full_simp_tac 1);
    4.60  qed"reduce_hd";
    4.61  
    4.62  
    4.63 @@ -154,7 +154,7 @@
    4.64  by (Asm_full_simp_tac 1);
    4.65  by (REPEAT (etac exE 1));
    4.66  by (Asm_full_simp_tac 1);
    4.67 -by (stac expand_if 1);
    4.68 +by (stac split_if 1);
    4.69  by (rtac conjI 1);
    4.70  by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
    4.71  by (Step_tac 1);
    4.72 @@ -167,7 +167,7 @@
    4.73            C h a n n e l   A b s t r a c t i o n
    4.74   *******************************************************************)
    4.75  
    4.76 -Delsplits [expand_if];
    4.77 +Delsplits [split_if];
    4.78  goal Correctness.thy 
    4.79        "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
    4.80  by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
    4.81 @@ -221,7 +221,7 @@
    4.82  by (rtac imp_conj_lemma 1);
    4.83  by (Action.action.induct_tac "a" 1);
    4.84  (* 7 cases *)
    4.85 -by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
    4.86 +by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
    4.87  qed"sender_unchanged";
    4.88  
    4.89  (* 2 copies of before *)
    4.90 @@ -237,7 +237,7 @@
    4.91  by (rtac imp_conj_lemma 1);
    4.92  by (Action.action.induct_tac "a" 1);
    4.93  (* 7 cases *)
    4.94 -by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
    4.95 +by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
    4.96  qed"receiver_unchanged";
    4.97  
    4.98  goal Correctness.thy 
    4.99 @@ -252,9 +252,9 @@
   4.100  by (rtac imp_conj_lemma 1);
   4.101  by (Action.action.induct_tac "a" 1);
   4.102  (* 7 cases *)
   4.103 -by (ALLGOALS (simp_tac ((simpset() addsimps [externals_def]) setloop (split_tac [expand_if]))));
   4.104 +by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
   4.105  qed"env_unchanged";
   4.106 -Addsplits [expand_if];
   4.107 +Addsplits [split_if];
   4.108  
   4.109  goal Correctness.thy "compatible srch_ioa rsch_ioa"; 
   4.110  by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
     5.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Apr 27 16:46:56 1998 +0200
     5.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Mon Apr 27 16:47:50 1998 +0200
     5.3 @@ -16,7 +16,7 @@
     5.4  val and_de_morgan_and_absorbe = result();
     5.5  
     5.6  goal HOL.thy "(if C then A else B) --> (A|B)";
     5.7 -by (stac expand_if 1);
     5.8 +by (stac split_if 1);
     5.9  by (Fast_tac 1);
    5.10  val bool_if_impl_or = result();
    5.11  
     6.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Mon Apr 27 16:46:56 1998 +0200
     6.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Mon Apr 27 16:47:50 1998 +0200
     6.3 @@ -68,7 +68,7 @@
     6.4  (* Proof of correctness *)
     6.5  goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
     6.6    "is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
     6.7 -by (simp_tac (simpset() delsplits [expand_if] addsimps 
     6.8 +by (simp_tac (simpset() delsplits [split_if] addsimps 
     6.9      [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
    6.10  by (rtac conjI 1);
    6.11   by (simp_tac ss' 1);
    6.12 @@ -77,7 +77,7 @@
    6.13  by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
    6.14  
    6.15  by (Action.action.induct_tac "a"  1);
    6.16 -by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
    6.17 +by (asm_simp_tac (ss' addsplits [split_if]) 1);
    6.18  by (forward_tac [inv4] 1);
    6.19  by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
    6.20  by (simp_tac ss' 1);
     7.1 --- a/src/HOLCF/IOA/NTP/Impl.ML	Mon Apr 27 16:46:56 1998 +0200
     7.2 +++ b/src/HOLCF/IOA/NTP/Impl.ML	Mon Apr 27 16:47:50 1998 +0200
     7.3 @@ -60,12 +60,8 @@
     7.4                     addsimps transitions);     
     7.5  val rename_ss = (ss addsimps unfold_renaming);
     7.6  
     7.7 -
     7.8 -
     7.9 -val tac     = asm_simp_tac ((ss addcongs [conj_cong]) 
    7.10 -                            setloop (split_tac [expand_if]));
    7.11 -val tac_ren = asm_simp_tac ((rename_ss addcongs [conj_cong]) 
    7.12 -                            setloop (split_tac [expand_if]));
    7.13 +val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]);
    7.14 +val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]);
    7.15  
    7.16  
    7.17  
    7.18 @@ -85,7 +81,7 @@
    7.19  
    7.20  (* First half *)
    7.21  by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
    7.22 -                                 delsplits [expand_if]) 1);
    7.23 +                                 delsplits [split_if]) 1);
    7.24  by (rtac Action.action.induct 1);
    7.25  
    7.26  by (EVERY1[tac, tac, tac, tac]);
    7.27 @@ -103,7 +99,7 @@
    7.28  
    7.29  (* Now the other half *)
    7.30  by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
    7.31 -                                 delsplits [expand_if]) 1);
    7.32 +                                 delsplits [split_if]) 1);
    7.33  by (rtac Action.action.induct 1);
    7.34  by (EVERY1[tac, tac]);
    7.35  
    7.36 @@ -114,7 +110,7 @@
    7.37  by (REPEAT (etac conjE 1));
    7.38  by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
    7.39                                        Multiset.countm_nonempty_def]
    7.40 -                            addsplits [expand_if]) 1);
    7.41 +                            addsplits [split_if]) 1);
    7.42  (* detour 2 *)
    7.43  by (tac 1);
    7.44  by (tac_ren 1);
    7.45 @@ -124,7 +120,7 @@
    7.46                                           Multiset.count_def,
    7.47                                           Multiset.countm_nonempty_def,
    7.48                                           Multiset.delm_nonempty_def]
    7.49 -                                 addsplits [expand_if]) 1);
    7.50 +                                 addsplits [split_if]) 1);
    7.51  by (rtac allI 1);
    7.52  by (rtac conjI 1);
    7.53  by (rtac impI 1);
    7.54 @@ -163,7 +159,7 @@
    7.55                             @ sender_projections @ impl_ioas)))
    7.56        1);
    7.57  
    7.58 -  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
    7.59 +  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
    7.60    by (Action.action.induct_tac "a" 1);
    7.61  
    7.62    (* 10 cases. First 4 are simple, since state doesn't change *)
    7.63 @@ -224,11 +220,10 @@
    7.64                      (Impl.inv3_def :: (receiver_projections 
    7.65                                         @ sender_projections @ impl_ioas))) 1);
    7.66  
    7.67 -  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
    7.68 +  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
    7.69    by (Action.action.induct_tac "a" 1);
    7.70  
    7.71 -val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] 
    7.72 -                              setloop (split_tac [expand_if]));
    7.73 +val tac3 = asm_full_simp_tac (ss addsimps [inv3_def] addsplits [split_if]);
    7.74  
    7.75    (* 10 - 8 *)
    7.76  
    7.77 @@ -291,11 +286,11 @@
    7.78                      (Impl.inv4_def :: (receiver_projections 
    7.79                                         @ sender_projections @ impl_ioas))) 1);
    7.80  
    7.81 -  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [expand_if]) 1);
    7.82 +  by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
    7.83    by (Action.action.induct_tac "a" 1);
    7.84  
    7.85  val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]
    7.86 -                              setloop (split_tac [expand_if]));
    7.87 +                              setloop (split_tac [split_if]));
    7.88  
    7.89    (* 10 - 2 *)
    7.90    
     8.1 --- a/src/HOLCF/IOA/NTP/Lemmas.ML	Mon Apr 27 16:46:56 1998 +0200
     8.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Mon Apr 27 16:47:50 1998 +0200
     8.3 @@ -36,7 +36,7 @@
     8.4  (* Arithmetic *)
     8.5  
     8.6  goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
     8.7 -by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
     8.8 +by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
     8.9  by (Blast_tac 1);
    8.10  qed "pred_suc";
    8.11  
     9.1 --- a/src/HOLCF/IOA/NTP/Multiset.ML	Mon Apr 27 16:46:56 1998 +0200
     9.2 +++ b/src/HOLCF/IOA/NTP/Multiset.ML	Mon Apr 27 16:47:50 1998 +0200
     9.3 @@ -15,27 +15,23 @@
     9.4  goal Multiset.thy 
     9.5       "count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
     9.6    by (asm_simp_tac (simpset() addsimps 
     9.7 -                    [Multiset.count_def,Multiset.countm_nonempty_def]
     9.8 -                    setloop (split_tac [expand_if])) 1);
     9.9 +                    [Multiset.count_def,Multiset.countm_nonempty_def]) 1);
    9.10  qed "count_addm_simp";
    9.11  
    9.12  goal Multiset.thy "count M y <= count (addm M x) y";
    9.13 -  by (simp_tac (simpset() addsimps [count_addm_simp]
    9.14 -                         setloop (split_tac [expand_if])) 1);
    9.15 +  by (simp_tac (simpset() addsimps [count_addm_simp]) 1);
    9.16  qed "count_leq_addm";
    9.17  
    9.18  goalw Multiset.thy [Multiset.count_def] 
    9.19       "count (delm M x) y = (if y=x then count M y - 1 else count M y)";
    9.20 -  by (res_inst_tac [("M","M")] Multiset.induction 1);
    9.21 -  by (asm_simp_tac (simpset() 
    9.22 -                   addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]
    9.23 -                   setloop (split_tac [expand_if])) 1);
    9.24 -  by (asm_full_simp_tac (simpset() 
    9.25 +by (res_inst_tac [("M","M")] Multiset.induction 1);
    9.26 +by (asm_simp_tac (simpset() 
    9.27 +             addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1);
    9.28 +by (asm_full_simp_tac (simpset() 
    9.29                           addsimps [Multiset.delm_nonempty_def,
    9.30 -                                   Multiset.countm_nonempty_def]
    9.31 -                         setloop (split_tac [expand_if])) 1);
    9.32 -  by Safe_tac;
    9.33 -  by (Asm_full_simp_tac 1);
    9.34 +                                   Multiset.countm_nonempty_def]) 1);
    9.35 +by Safe_tac;
    9.36 +by (Asm_full_simp_tac 1);
    9.37  qed "count_delm_simp";
    9.38  
    9.39  goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
    9.40 @@ -50,8 +46,7 @@
    9.41    by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
    9.42                                     Multiset.countm_empty_def]) 1);
    9.43    by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
    9.44 -                                      Multiset.delm_nonempty_def]
    9.45 -                             setloop (split_tac [expand_if])) 1);
    9.46 +                                      Multiset.delm_nonempty_def]) 1);
    9.47  qed "countm_spurious_delm";
    9.48  
    9.49  
    9.50 @@ -62,8 +57,7 @@
    9.51                             Multiset.countm_empty_def]) 1);
    9.52    by (asm_simp_tac (simpset() addsimps 
    9.53                         [Multiset.count_def,Multiset.delm_nonempty_def,
    9.54 -                        Multiset.countm_nonempty_def]
    9.55 -                    setloop (split_tac [expand_if])) 1);
    9.56 +                        Multiset.countm_nonempty_def]) 1);
    9.57  qed_spec_mp "pos_count_imp_pos_countm";
    9.58  
    9.59  goal Multiset.thy
    9.60 @@ -74,8 +68,7 @@
    9.61                             Multiset.countm_empty_def]) 1);
    9.62    by (asm_simp_tac (simpset() addsimps 
    9.63                        [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
    9.64 -                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]
    9.65 -                    addsplits [expand_if]) 1);
    9.66 +                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
    9.67  qed "countm_done_delm";
    9.68  
    9.69  
    10.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Apr 27 16:46:56 1998 +0200
    10.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Mon Apr 27 16:47:50 1998 +0200
    10.3 @@ -511,7 +511,7 @@
    10.4  temp_sat_def, satisfies_def,Next_def]
    10.5  "!! h. [| temp_strengthening P Q h |]\
    10.6  \      ==> temp_strengthening (Next P) (Next Q) h";
    10.7 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    10.8 +by (Asm_full_simp_tac 1);
    10.9  by (safe_tac set_cs);
   10.10  by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
   10.11  by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU]) 1);
    11.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Apr 27 16:46:56 1998 +0200
    11.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Apr 27 16:47:50 1998 +0200
    11.3 @@ -393,8 +393,7 @@
    11.4  \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
    11.5  
    11.6    by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
    11.7 -                            ioa_projections)
    11.8 -                  setloop (split_tac [expand_if])) 1);
    11.9 +                            ioa_projections)) 1);
   11.10  qed "trans_of_par4";
   11.11  
   11.12  
    12.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Apr 27 16:46:56 1998 +0200
    12.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Apr 27 16:47:50 1998 +0200
    12.3 @@ -132,8 +132,7 @@
    12.4  
    12.5  goal thy "stutter sig (s, (a,t)>>ex) = \
    12.6  \     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
    12.7 -by (simp_tac (simpset() addsimps [stutter_def] 
    12.8 -                       setloop (split_tac [expand_if]) ) 1);
    12.9 +by (simp_tac (simpset() addsimps [stutter_def]) 1);
   12.10  qed"stutter_cons";
   12.11  
   12.12  (* ----------------------------------------------------------------------------------- *)
   12.13 @@ -167,8 +166,7 @@
   12.14  (* main case *)
   12.15  ren "ss a t" 1;
   12.16  by (safe_tac set_cs);
   12.17 -by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
   12.18 -                       setloop (split_tac [expand_if])) 1));
   12.19 +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
   12.20  qed"lemma_1_1a";
   12.21  
   12.22  
   12.23 @@ -183,8 +181,7 @@
   12.24  by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
   12.25  (* main case *)
   12.26  by (safe_tac set_cs);
   12.27 -by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2
   12.28 -                 setloop (split_tac [expand_if])) 1));
   12.29 +by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
   12.30  qed"lemma_1_1b";
   12.31  
   12.32  
    13.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Apr 27 16:46:56 1998 +0200
    13.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Apr 27 16:47:50 1998 +0200
    13.3 @@ -112,8 +112,7 @@
    13.4  goal thy "!!x.[| x:act A; x~:act B |] \
    13.5  \   ==> mkex A B (x>>sch) (s,a>>exA) (t,exB)  =  \
    13.6  \       ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
    13.7 -by (simp_tac (simpset() addsimps [mkex_def] 
    13.8 -                       setloop (split_tac [expand_if]) ) 1);
    13.9 +by (simp_tac (simpset() addsimps [mkex_def]) 1);
   13.10  by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
   13.11  by Auto_tac;
   13.12  qed"mkex_cons_1";
   13.13 @@ -121,8 +120,7 @@
   13.14  goal thy "!!x.[| x~:act A; x:act B |] \
   13.15  \   ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =  \ 
   13.16  \       ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
   13.17 -by (simp_tac (simpset() addsimps [mkex_def] 
   13.18 -                       setloop (split_tac [expand_if]) ) 1);
   13.19 +by (simp_tac (simpset() addsimps [mkex_def]) 1);
   13.20  by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
   13.21  by Auto_tac;
   13.22  qed"mkex_cons_2";
   13.23 @@ -130,8 +128,7 @@
   13.24  goal thy "!!x.[| x:act A; x:act B |]  \
   13.25  \   ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
   13.26  \        ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
   13.27 -by (simp_tac (simpset() addsimps [mkex_def] 
   13.28 -                       setloop (split_tac [expand_if]) ) 1);
   13.29 +by (simp_tac (simpset() addsimps [mkex_def]) 1);
   13.30  by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
   13.31  by Auto_tac;
   13.32  qed"mkex_cons_3";
   13.33 @@ -216,7 +213,7 @@
   13.34  
   13.35  (* main case *) 
   13.36  (* splitting into 4 cases according to a:A, a:B *)
   13.37 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   13.38 +by (Asm_full_simp_tac 1);
   13.39  by (safe_tac set_cs);
   13.40  
   13.41  (* Case y:A, y:B *)
   13.42 @@ -249,7 +246,7 @@
   13.43  
   13.44  fun mkex_induct_tac sch exA exB = 
   13.45      EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], 
   13.46 -           asm_full_simp_tac (simpset() setloop split_tac [expand_if]),
   13.47 +           Asm_full_simp_tac,
   13.48             SELECT_GOAL (safe_tac set_cs),
   13.49             Seq_case_simp_tac exA,
   13.50             Seq_case_simp_tac exB,
    14.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Apr 27 16:46:56 1998 +0200
    14.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Apr 27 16:47:50 1998 +0200
    14.3 @@ -209,7 +209,7 @@
    14.4  by (etac Seq_Finite_ind  1);
    14.5  by (Asm_full_simp_tac 1);
    14.6  (* main case *)
    14.7 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    14.8 +by (Asm_full_simp_tac 1);
    14.9  by (safe_tac set_cs);
   14.10  
   14.11  (* a: act A; a: act B *)
   14.12 @@ -479,7 +479,7 @@
   14.13  
   14.14  (* main case *) 
   14.15  (* splitting into 4 cases according to a:A, a:B *)
   14.16 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   14.17 +by (Asm_full_simp_tac 1);
   14.18  by (safe_tac set_cs);
   14.19  
   14.20  (* Case a:A, a:B *)
    15.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Apr 27 16:46:56 1998 +0200
    15.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Apr 27 16:47:50 1998 +0200
    15.3 @@ -50,7 +50,7 @@
    15.4      Needs compositionality on schedule level, input-enabledness, compatibility
    15.5                      and distributivity of is_exec_frag over @@
    15.6  **********************************************************************************)
    15.7 -Delsplits [expand_if];
    15.8 +Delsplits [split_if];
    15.9  goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
   15.10  \            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
   15.11  \          ==> (sch @@ a>>nil) : schedules (A||B)";
   15.12 @@ -83,7 +83,7 @@
   15.13  by (REPEAT (atac 1));
   15.14  qed"IOA_deadlock_free";
   15.15  
   15.16 -Addsplits [expand_if];
   15.17 +Addsplits [split_if];
   15.18  
   15.19  
   15.20  
    16.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Apr 27 16:46:56 1998 +0200
    16.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Apr 27 16:47:50 1998 +0200
    16.3 @@ -129,7 +129,7 @@
    16.4  (* ------------------------------------------------------
    16.5                   Lemma 1 :Traces coincide  
    16.6     ------------------------------------------------------- *)
    16.7 -Delsplits[expand_if];
    16.8 +Delsplits[split_if];
    16.9  goalw thy [corresp_ex_def]
   16.10    "!!f.[|is_ref_map f C A; ext C = ext A|] ==>  \     
   16.11  \        !s. reachable C s & is_exec_frag C (s,xs) --> \
   16.12 @@ -144,9 +144,9 @@
   16.13  by (eres_inst_tac [("x","y")] allE 1);
   16.14  by (Asm_full_simp_tac 1);
   16.15  by (asm_full_simp_tac (simpset() addsimps [move_subprop4] 
   16.16 -                          setloop split_tac [expand_if] ) 1);
   16.17 +                          addsplits [split_if]) 1);
   16.18  qed"lemma_1";
   16.19 -Addsplits[expand_if];
   16.20 +Addsplits[split_if];
   16.21  
   16.22  (* ------------------------------------------------------------------ *)
   16.23  (*                   The following lemmata contribute to              *)
    17.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Apr 27 16:46:56 1998 +0200
    17.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Apr 27 16:47:50 1998 +0200
    17.3 @@ -68,7 +68,7 @@
    17.4    by (fast_tac (claset() addDs prems) 1);
    17.5  val lemma = result();
    17.6  
    17.7 -Delsplits [expand_if];
    17.8 +Delsplits [split_if];
    17.9  goal thy "!!f.[| is_weak_ref_map f C A |]\
   17.10  \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
   17.11  by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   17.12 @@ -82,7 +82,7 @@
   17.13  by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,
   17.14  asig_outputs_def,asig_of_def,trans_of_def]) 1);
   17.15  by Safe_tac;
   17.16 -by (stac expand_if 1);
   17.17 +by (stac split_if 1);
   17.18   by (rtac conjI 1);
   17.19   by (rtac impI 1);
   17.20   by (etac disjE 1);
   17.21 @@ -111,6 +111,6 @@
   17.22  by (forward_tac  [reachable_rename] 1);
   17.23  by Auto_tac;
   17.24  qed"rename_through_pmap";
   17.25 -Addsplits [expand_if];
   17.26 +Addsplits [split_if];
   17.27  
   17.28  
    18.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Apr 27 16:46:56 1998 +0200
    18.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Apr 27 16:47:50 1998 +0200
    18.3 @@ -120,7 +120,7 @@
    18.4  goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
    18.5  by (simp_tac (simpset() addsimps [Last_def, Cons_def]) 1);
    18.6  by (res_inst_tac [("x","xs")] seq.casedist 1);
    18.7 -by (asm_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    18.8 +by (Asm_simp_tac 1);
    18.9  by (REPEAT (Asm_simp_tac 1));
   18.10  qed"Last_cons";
   18.11  
   18.12 @@ -699,7 +699,7 @@
   18.13  by (Simp_tac 1);
   18.14  by (Simp_tac 1);
   18.15  (* main case *)
   18.16 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if] ) 1);
   18.17 +by (Asm_full_simp_tac 1);
   18.18  qed"FilternPnilForallP1";
   18.19  
   18.20  bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
   18.21 @@ -1158,8 +1158,7 @@
   18.22  (* FIX: better support for A = %x. True *)
   18.23  by (Fast_tac 3);
   18.24  by (asm_full_simp_tac (simpset() addsimps [Filter_lemma1]) 1);
   18.25 -by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3] 
   18.26 -                                setloop split_tac [expand_if]) 1);
   18.27 +by (asm_full_simp_tac (simpset() addsimps [Filter_lemma2,Filter_lemma3]) 1);
   18.28  qed"FilterPQ_takelemma";
   18.29  
   18.30  Addsimps [FilterPQ];
    19.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Mon Apr 27 16:46:56 1998 +0200
    19.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Mon Apr 27 16:47:50 1998 +0200
    19.3 @@ -156,7 +156,7 @@
    19.4                   Lemma 1 :Traces coincide  
    19.5     ------------------------------------------------------- *)
    19.6  
    19.7 -Delsplits[expand_if];
    19.8 +Delsplits[split_if];
    19.9  goal thy 
   19.10    "!!f.[|is_simulation R C A; ext C = ext A|] ==>  \     
   19.11  \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
   19.12 @@ -177,9 +177,9 @@
   19.13  by (asm_full_simp_tac (simpset() addsimps 
   19.14        [rewrite_rule [Let_def] move_subprop5_sim,
   19.15         rewrite_rule [Let_def] move_subprop4_sim] 
   19.16 -   setloop split_tac [expand_if] ) 1);
   19.17 +   addsplits [split_if]) 1);
   19.18  qed_spec_mp"traces_coincide_sim";
   19.19 -Addsplits[expand_if];
   19.20 +Addsplits[split_if];
   19.21  
   19.22  
   19.23  (* ----------------------------------------------------------- *)
    20.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Mon Apr 27 16:46:56 1998 +0200
    20.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Mon Apr 27 16:47:50 1998 +0200
    20.3 @@ -138,7 +138,7 @@
    20.4  
    20.5  val tsuffix_TL2 = conjI RS tsuffix_TL;
    20.6  
    20.7 -Delsplits[expand_if];
    20.8 +Delsplits[split_if];
    20.9  goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
   20.10     "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
   20.11  auto();
   20.12 @@ -146,33 +146,33 @@
   20.13  by (eres_inst_tac [("x","s")] allE 1);
   20.14  by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
   20.15  (* []F .--> Next [] F *)
   20.16 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   20.17 +by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
   20.18  auto();
   20.19  bd tsuffix_TL2 1;
   20.20  by (REPEAT (atac 1));
   20.21  auto();
   20.22  qed"LTL1";
   20.23 -Addsplits[expand_if];
   20.24 +Addsplits[split_if];
   20.25  
   20.26  
   20.27  goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
   20.28      "s |= .~ (Next F) .--> (Next (.~ F))";
   20.29 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   20.30 +by (Asm_full_simp_tac 1);
   20.31  qed"LTL2a";
   20.32  
   20.33  goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
   20.34      "s |= (Next (.~ F)) .--> (.~ (Next F))";
   20.35 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   20.36 +by (Asm_full_simp_tac 1);
   20.37  qed"LTL2b";
   20.38  
   20.39  goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
   20.40  "ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
   20.41 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   20.42 +by (Asm_full_simp_tac 1);
   20.43  qed"LTL3";
   20.44  
   20.45  goalw thy [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
   20.46   "s |= [] (F .--> Next F) .--> F .--> []F";
   20.47 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   20.48 +by (Asm_full_simp_tac 1);
   20.49  auto();
   20.50  
   20.51  
    21.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Apr 27 16:46:56 1998 +0200
    21.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Mon Apr 27 16:47:50 1998 +0200
    21.3 @@ -84,7 +84,7 @@
    21.4  \  ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \
    21.5  \             .--> (Next (Init (%(s,a,t).Q s))))";
    21.6  
    21.7 -by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
    21.8 +by (Asm_full_simp_tac 1);
    21.9  by (pair_tac "ex" 1);
   21.10  by (Seq_case_simp_tac "y" 1);
   21.11  
    22.1 --- a/src/HOLCF/Lift3.ML	Mon Apr 27 16:46:56 1998 +0200
    22.2 +++ b/src/HOLCF/Lift3.ML	Mon Apr 27 16:47:50 1998 +0200
    22.3 @@ -94,12 +94,6 @@
    22.4  by (fast_tac (HOL_cs addSEs prems) 1);
    22.5  qed"Lift_cases";
    22.6  
    22.7 -goal thy
    22.8 -  "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
    22.9 -by (lift.induct_tac "x" 1);
   22.10 -by (ALLGOALS Asm_simp_tac);
   22.11 -qed "expand_lift_case";
   22.12 -
   22.13  goal thy "(x~=UU)=(? y. x=Def y)";
   22.14  by (rtac iffI 1);
   22.15  by (rtac Lift_cases 1);
    23.1 --- a/src/HOLCF/Sprod0.ML	Mon Apr 27 16:46:56 1998 +0200
    23.2 +++ b/src/HOLCF/Sprod0.ML	Mon Apr 27 16:47:50 1998 +0200
    23.3 @@ -19,11 +19,11 @@
    23.4          (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl])
    23.5          ]);
    23.6  
    23.7 -qed_goal "inj_onto_Abs_Sprod" Sprod0.thy 
    23.8 -        "inj_onto Abs_Sprod Sprod"
    23.9 +qed_goal "inj_on_Abs_Sprod" Sprod0.thy 
   23.10 +        "inj_on Abs_Sprod Sprod"
   23.11  (fn prems =>
   23.12          [
   23.13 -        (rtac inj_onto_inverseI 1),
   23.14 +        (rtac inj_on_inverseI 1),
   23.15          (etac Abs_Sprod_inverse 1)
   23.16          ]);
   23.17  
   23.18 @@ -80,7 +80,7 @@
   23.19          (cut_facts_tac prems 1),
   23.20          (etac inject_Spair_Rep 1),
   23.21          (atac 1),
   23.22 -        (etac (inj_onto_Abs_Sprod  RS inj_ontoD) 1),
   23.23 +        (etac (inj_on_Abs_Sprod  RS inj_onD) 1),
   23.24          (rtac SprodI 1),
   23.25          (rtac SprodI 1)
   23.26          ]);
   23.27 @@ -132,7 +132,7 @@
   23.28          [
   23.29          (cut_facts_tac prems 1),
   23.30          (rtac defined_Spair_Rep_rev 1),
   23.31 -        (rtac (inj_onto_Abs_Sprod  RS inj_ontoD) 1),
   23.32 +        (rtac (inj_on_Abs_Sprod  RS inj_onD) 1),
   23.33          (atac 1),
   23.34          (rtac SprodI 1),
   23.35          (rtac SprodI 1)
    24.1 --- a/src/HOLCF/Ssum0.ML	Mon Apr 27 16:46:56 1998 +0200
    24.2 +++ b/src/HOLCF/Ssum0.ML	Mon Apr 27 16:47:50 1998 +0200
    24.3 @@ -30,10 +30,10 @@
    24.4          (rtac refl 1)
    24.5          ]);
    24.6  
    24.7 -qed_goal "inj_onto_Abs_Ssum" Ssum0.thy "inj_onto Abs_Ssum Ssum"
    24.8 +qed_goal "inj_on_Abs_Ssum" Ssum0.thy "inj_on Abs_Ssum Ssum"
    24.9  (fn prems =>
   24.10          [
   24.11 -        (rtac inj_onto_inverseI 1),
   24.12 +        (rtac inj_on_inverseI 1),
   24.13          (etac Abs_Ssum_inverse 1)
   24.14          ]);
   24.15  
   24.16 @@ -89,7 +89,7 @@
   24.17          [
   24.18          (cut_facts_tac prems 1),
   24.19          (rtac noteq_SinlSinr_Rep 1),
   24.20 -        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
   24.21 +        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
   24.22          (rtac SsumIl 1),
   24.23          (rtac SsumIr 1)
   24.24          ]);
   24.25 @@ -184,7 +184,7 @@
   24.26          [
   24.27          (cut_facts_tac prems 1),
   24.28          (rtac inject_Sinl_Rep 1),
   24.29 -        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
   24.30 +        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
   24.31          (rtac SsumIl 1),
   24.32          (rtac SsumIl 1)
   24.33          ]);
   24.34 @@ -195,7 +195,7 @@
   24.35          [
   24.36          (cut_facts_tac prems 1),
   24.37          (rtac inject_Sinr_Rep 1),
   24.38 -        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
   24.39 +        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
   24.40          (rtac SsumIr 1),
   24.41          (rtac SsumIr 1)
   24.42          ]);
    25.1 --- a/src/HOLCF/Tr.ML	Mon Apr 27 16:46:56 1998 +0200
    25.2 +++ b/src/HOLCF/Tr.ML	Mon Apr 27 16:47:50 1998 +0200
    25.3 @@ -99,10 +99,10 @@
    25.4    "P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))";
    25.5  by (res_inst_tac [("p","Q")] trE 1);
    25.6  by (REPEAT (Asm_full_simp_tac 1));
    25.7 -qed"expand_If2";
    25.8 +qed"split_If2";
    25.9  
   25.10  val split_If_tac =
   25.11 -  simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [expand_If2]);
   25.12 +  simp_tac (HOL_basic_ss addsimps [symmetric If2_def]) THEN' (split_tac [split_If2]);
   25.13  
   25.14   
   25.15