equal
deleted
inserted
replaced
89 where |
89 where |
90 "neg_not_seq x = (%i. case Lazy_Sequence.yield (x i) of |
90 "neg_not_seq x = (%i. case Lazy_Sequence.yield (x i) of |
91 None => Lazy_Sequence.hb_single () |
91 None => Lazy_Sequence.hb_single () |
92 | Some ((), xq) => Lazy_Sequence.empty)" |
92 | Some ((), xq) => Lazy_Sequence.empty)" |
93 |
93 |
94 hide (open) type pos_dseq neg_dseq |
94 hide_type (open) pos_dseq neg_dseq |
95 |
95 |
96 hide (open) const |
96 hide_const (open) |
97 pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map |
97 pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map |
98 neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map |
98 neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map |
99 hide (open) fact |
99 hide_fact (open) |
100 pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def |
100 pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def |
101 neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def |
101 neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def |
102 |
102 |
103 end |
103 end |