changeset 35215 | a03462cbf86f |
parent 35174 | e15040ae75d7 |
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Feb 18 12:36:09 2010 -0800 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Thu Feb 18 13:29:59 2010 -0800 @@ -165,7 +165,7 @@ (* --------------------------------------------------- *) lemma mk_traceConc: "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)" -apply (simp add: mk_trace_def filter_act_def FilterConc MapConc) +apply (simp add: mk_trace_def filter_act_def MapConc) done