src/HOL/IOA/Solve.ML
changeset 5184 9b8547a9496a
parent 5143 b94cd208f073
child 6916 4957978b6f9e
     1.1 --- a/src/HOL/IOA/Solve.ML	Fri Jul 24 13:03:20 1998 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Fri Jul 24 13:19:38 1998 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4  by (asm_full_simp_tac
     1.5        (simpset() addsimps [executions_def,is_execution_fragment_def,
     1.6                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
     1.7 -                addsplits [split_option_case]) 1);
     1.8 +                addsplits [option.split]) 1);
     1.9  qed"comp1_reachable";
    1.10  
    1.11  
    1.12 @@ -99,7 +99,7 @@
    1.13  by (asm_full_simp_tac
    1.14        (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.15                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.16 -                addsplits [split_option_case]) 1);
    1.17 +                addsplits [option.split]) 1);
    1.18  qed"comp2_reachable";
    1.19  
    1.20  Delsplits [split_if];
    1.21 @@ -161,7 +161,7 @@
    1.22  by (asm_full_simp_tac
    1.23        (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.24                            par_def,starts_of_def,trans_of_def,rename_def]
    1.25 -                addsplits [split_option_case]) 1);
    1.26 +                addsplits [option.split]) 1);
    1.27  by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
    1.28  qed"reachable_rename_ioa";
    1.29