equal
deleted
inserted
replaced
194 dummy sort: it is effectively ignored in type-inference. |
194 dummy sort: it is effectively ignored in type-inference. |
195 |
195 |
196 |
196 |
197 *** HOL *** |
197 *** HOL *** |
198 |
198 |
199 * Abstract bit operations as part of Main: push_bit, push_take, |
199 * Abstract bit operations as part of Main: push_bit, take_bit, |
200 push_drop. |
200 drop_bit. |
201 |
201 |
202 * New, more general, axiomatization of complete_distrib_lattice. |
202 * New, more general, axiomatization of complete_distrib_lattice. |
203 The former axioms: |
203 The former axioms: |
204 "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" |
204 "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" |
205 are replaced by |
205 are replaced by |