equal
deleted
inserted
replaced
103 |
103 |
104 goal IOA.thy |
104 goal IOA.thy |
105 "actions(asig_comp a b) = actions(a) Un actions(b)"; |
105 "actions(asig_comp a b) = actions(a) Un actions(b)"; |
106 by(simp_tac (!simpset addsimps |
106 by(simp_tac (!simpset addsimps |
107 ([actions_def,asig_comp_def]@asig_projections)) 1); |
107 ([actions_def,asig_comp_def]@asig_projections)) 1); |
108 by(fast_tac eq_cs 1); |
108 by(Fast_tac 1); |
109 qed "actions_asig_comp"; |
109 qed "actions_asig_comp"; |
110 |
110 |
111 goal IOA.thy |
111 goal IOA.thy |
112 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; |
112 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; |
113 by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); |
113 by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); |