changeset 44066 | d74182c93f04 |
parent 42793 | 88bee9f6eec7 |
child 45606 | b1e1508643b1 |
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Mon Aug 08 10:26:26 2011 -0700 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Mon Aug 08 10:32:55 2011 -0700 @@ -609,7 +609,7 @@ (if a:actions(asig_of(D)) then (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) else snd(snd(snd(t)))=snd(snd(snd(s)))))" - apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq Let_def ioa_projections) + apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections) done