equal
deleted
inserted
replaced
95 end; |
95 end; |
96 *} |
96 *} |
97 |
97 |
98 code_reserved Eval DSequence |
98 code_reserved Eval DSequence |
99 (* |
99 (* |
100 hide type Sequence.seq |
100 hide_type Sequence.seq |
101 |
101 |
102 hide const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single |
102 hide_const Sequence.Seq Sequence.yield Sequence.yieldn Sequence.empty Sequence.single |
103 Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq |
103 Sequence.append Sequence.flat Sequence.map Sequence.bind Sequence.ifpred Sequence.not_seq |
104 *) |
104 *) |
105 hide (open) const empty single eval map_seq bind union if_seq not_seq map |
105 hide_const (open) empty single eval map_seq bind union if_seq not_seq map |
106 hide (open) fact empty_def single_def eval.simps map_seq.simps bind_def union_def |
106 hide_fact (open) empty_def single_def eval.simps map_seq.simps bind_def union_def |
107 if_seq_def not_seq_def map_def |
107 if_seq_def not_seq_def map_def |
108 |
108 |
109 end |
109 end |