equal
deleted
inserted
replaced
102 |
102 |
103 |
103 |
104 (* Restrict the trace to those members of the set s *) |
104 (* Restrict the trace to those members of the set s *) |
105 filter_oseq_def |
105 filter_oseq_def |
106 "filter_oseq p s == |
106 "filter_oseq p s == |
107 (%i.case s(i) |
107 (%i. case s(i) |
108 of None => None |
108 of None => None |
109 | Some(x) => if p x then Some x else None)" |
109 | Some(x) => if p x then Some x else None)" |
110 |
110 |
111 |
111 |
112 mk_trace_def |
112 mk_trace_def |
113 "mk_trace(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))" |
113 "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))" |
114 |
114 |
115 |
115 |
116 (* Does an ioa have an execution with the given trace *) |
116 (* Does an ioa have an execution with the given trace *) |
117 has_trace_def |
117 has_trace_def |
118 "has_trace ioa b == |
118 "has_trace ioa b == |