equal
deleted
inserted
replaced
16 |
16 |
17 by (simp_tac(SS addsimps [has_behaviour_def])1); |
17 by (simp_tac(SS addsimps [has_behaviour_def])1); |
18 by (safe_tac set_cs); |
18 by (safe_tac set_cs); |
19 |
19 |
20 (* give execution of abstract automata *) |
20 (* give execution of abstract automata *) |
21 by (res_inst_tac[("x","<mk_behaviour A (fst ex),%i.f(snd ex i)>")] bexI 1); |
21 by (res_inst_tac[("x","(mk_behaviour A (fst ex),%i.f(snd ex i))")] bexI 1); |
22 |
22 |
23 (* Behaviours coincide *) |
23 (* Behaviours coincide *) |
24 by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1); |
24 by (asm_simp_tac (SS addsimps [mk_behaviour_def,filter_oseq_idemp])1); |
25 |
25 |
26 (* Use lemma *) |
26 (* Use lemma *) |