src/HOL/IOA/Solve.ML
changeset 3842 b55686a7b22c
parent 3078 984866a8f905
child 3919 c036caebfc75
     1.1 --- a/src/HOL/IOA/Solve.ML	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Fri Oct 10 19:02:28 1997 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    by (Asm_full_simp_tac 1);
     1.5  
     1.6    (* give execution of abstract automata *)
     1.7 -  by (res_inst_tac[("x","(mk_trace A (fst ex),%i.f(snd ex i))")] bexI 1);
     1.8 +  by (res_inst_tac[("x","(mk_trace A (fst ex),%i. f(snd ex i))")] bexI 1);
     1.9  
    1.10    (* Traces coincide *)
    1.11    by (asm_simp_tac (!simpset addsimps [mk_trace_def,filter_oseq_idemp])1);
    1.12 @@ -68,9 +68,9 @@
    1.13  by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); 
    1.14  by (etac bexE 1);
    1.15  by (res_inst_tac [("x",
    1.16 -   "(filter_oseq (%a.a:actions(asig_of(C1))) \
    1.17 +   "(filter_oseq (%a. a:actions(asig_of(C1))) \
    1.18  \                (fst ex),                                                \
    1.19 -\    %i.fst (snd ex i))")]  bexI 1);
    1.20 +\    %i. fst (snd ex i))")]  bexI 1);
    1.21  (* fst(s) is in projected execution *)
    1.22   by (Simp_tac 1);
    1.23   by (Fast_tac 1);
    1.24 @@ -88,9 +88,9 @@
    1.25  by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); 
    1.26  by (etac bexE 1);
    1.27  by (res_inst_tac [("x",
    1.28 -   "(filter_oseq (%a.a:actions(asig_of(C2)))\
    1.29 +   "(filter_oseq (%a. a:actions(asig_of(C2)))\
    1.30  \                (fst ex),                                                \
    1.31 -\    %i.snd (snd ex i))")]  bexI 1);
    1.32 +\    %i. snd (snd ex i))")]  bexI 1);
    1.33  (* fst(s) is in projected execution *)
    1.34   by (Simp_tac 1);
    1.35   by (Fast_tac 1);