src/HOL/IOA/Solve.ML
changeset 4831 dae4d63a1318
parent 4828 ee3317896a47
child 4838 196100237656
     1.1 --- a/src/HOL/IOA/Solve.ML	Mon Apr 27 16:45:11 1998 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Mon Apr 27 16:45:27 1998 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4                  addsplits [split_option_case]) 1);
     1.5  qed"comp2_reachable";
     1.6  
     1.7 -Delsplits [expand_if];
     1.8 +Delsplits [split_if];
     1.9  
    1.10  (* Composition of possibility-mappings *)
    1.11  goalw Solve.thy [is_weak_pmap_def] "!!f g.[| is_weak_pmap f C1 A1 & \
    1.12 @@ -121,7 +121,7 @@
    1.13  by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
    1.14  by (simp_tac (simpset() addsimps [par_def]) 1);
    1.15  by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
    1.16 -by (stac expand_if 1);
    1.17 +by (stac split_if 1);
    1.18  by (rtac conjI 1);
    1.19  by (rtac impI 1); 
    1.20  by (etac disjE 1);
    1.21 @@ -142,7 +142,7 @@
    1.22  by (Asm_full_simp_tac 2);
    1.23  by (Fast_tac 2);
    1.24  by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
    1.25 -                 addsplits [expand_if]) 1);
    1.26 +                 addsplits [split_if]) 1);
    1.27  by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    1.28          asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    1.29                                        comp2_reachable])1));
    1.30 @@ -176,7 +176,7 @@
    1.31  by (simp_tac (simpset() addsimps [rename_def]) 1);
    1.32  by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
    1.33  by Safe_tac;
    1.34 -by (stac expand_if 1);
    1.35 +by (stac split_if 1);
    1.36   by (rtac conjI 1);
    1.37   by (rtac impI 1);
    1.38   by (etac disjE 1);
    1.39 @@ -209,4 +209,4 @@
    1.40  by Auto_tac;
    1.41  qed"rename_through_pmap";
    1.42  
    1.43 -Addsplits [expand_if];
    1.44 +Addsplits [split_if];