equal
deleted
inserted
replaced
391 \ (if a:actions(asig_of(D)) then \ |
391 \ (if a:actions(asig_of(D)) then \ |
392 \ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ |
392 \ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \ |
393 \ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; |
393 \ else snd(snd(snd(t)))=snd(snd(snd(s)))))"; |
394 |
394 |
395 by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@ |
395 by (simp_tac (simpset() addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@ |
396 ioa_projections) |
396 ioa_projections)) 1); |
397 setloop (split_tac [expand_if])) 1); |
|
398 qed "trans_of_par4"; |
397 qed "trans_of_par4"; |
399 |
398 |
400 |
399 |
401 (* ---------------------------------------------------------------------------------- *) |
400 (* ---------------------------------------------------------------------------------- *) |
402 |
401 |