src/HOL/IOA/Solve.ML
changeset 4838 196100237656
parent 4831 dae4d63a1318
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/IOA/Solve.ML	Mon Apr 27 19:30:40 1998 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Mon Apr 27 19:32:19 1998 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4  \    %i. fst (snd ex i))")]  bexI 1);
     1.5  (* fst(s) is in projected execution *)
     1.6   by (Simp_tac 1);
     1.7 - by (fast_tac (claset() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
     1.8 + by (fast_tac (claset() delSWrapper"split_all_tac")1);
     1.9  (* projected execution is indeed an execution *)
    1.10  by (asm_full_simp_tac
    1.11        (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.12 @@ -94,7 +94,7 @@
    1.13  \    %i. snd (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() delWrapper"split_all_tac" delSWrapper"split_all_tac")1);
    1.17 + by (fast_tac (claset() 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,