src/HOL/IOA/Solve.ML
changeset 4799 82b0ed20c2cb
parent 4772 8c7e7eaffbdf
child 4828 ee3317896a47
     1.1 --- a/src/HOL/IOA/Solve.ML	Sat Apr 04 14:30:19 1998 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Tue Apr 07 13:43:07 1998 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
     1.5  
     1.6    by (simp_tac(simpset() addsimps [has_trace_def])1);
     1.7 -  by Safe_tac;
     1.8 +  by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
     1.9    by (rename_tac "f ex1 ex2" 1);
    1.10  
    1.11    (* choose same trace, therefore same NF *)
    1.12 @@ -74,12 +74,12 @@
    1.13  \    %i. fst (snd ex i))")]  bexI 1);
    1.14  (* fst(s) is in projected execution *)
    1.15   by (Simp_tac 1);
    1.16 - by (fast_tac (claset() delSWrapper "split_all_tac") 1);
    1.17 + by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
    1.18  (* projected execution is indeed an execution *)
    1.19  by (asm_full_simp_tac
    1.20        (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.21                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.22 -                addsplits [expand_if,split_option_case]) 1);
    1.23 +                addsplits [split_option_case]) 1);
    1.24  qed"comp1_reachable";
    1.25  
    1.26  
    1.27 @@ -94,12 +94,12 @@
    1.28  \    %i. snd (snd ex i))")]  bexI 1);
    1.29  (* fst(s) is in projected execution *)
    1.30   by (Simp_tac 1);
    1.31 - by (fast_tac (claset() delSWrapper "split_all_tac") 1);
    1.32 + by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
    1.33  (* projected execution is indeed an execution *)
    1.34  by (asm_full_simp_tac
    1.35        (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.36                            par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.37 -                addsplits [expand_if,split_option_case]) 1);
    1.38 +                addsplits [split_option_case]) 1);
    1.39  qed"comp2_reachable";
    1.40  
    1.41  Delsplits [expand_if];