equal
deleted
inserted
replaced
163 (* --------------------------------------------------- *) |
163 (* --------------------------------------------------- *) |
164 (* Lemma 1.1: Distribution of mk_trace and @@ *) |
164 (* Lemma 1.1: Distribution of mk_trace and @@ *) |
165 (* --------------------------------------------------- *) |
165 (* --------------------------------------------------- *) |
166 |
166 |
167 lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)" |
167 lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)" |
168 apply (simp add: mk_trace_def filter_act_def FilterConc MapConc) |
168 apply (simp add: mk_trace_def filter_act_def MapConc) |
169 done |
169 done |
170 |
170 |
171 |
171 |
172 |
172 |
173 (* ------------------------------------------------------ |
173 (* ------------------------------------------------------ |