# HG changeset patch # User haftmann # Date 1521798720 -3600 # Node ID 7f5b1b6f7f40ca918289a0939597a945cade7321 # Parent 0b70405b39698f7ff3179869c7da76a8495925b3 NEWS and CONTRIBUTORS diff -r 0b70405b3969 -r 7f5b1b6f7f40 CONTRIBUTORS --- a/CONTRIBUTORS Thu Mar 22 17:18:33 2018 +0100 +++ b/CONTRIBUTORS Fri Mar 23 10:52:00 2018 +0100 @@ -6,6 +6,11 @@ Contributions to this Isabelle version -------------------------------------- +* March 2018: Florian Haftmann + Abstract bit operations push_bit, push_take, push_drop, alongside + with an algebraic foundation for bit strings and word types in + HOL-ex. + * March 2018: Viorel Preoteasa Generalisation of complete_distrib_lattice diff -r 0b70405b3969 -r 7f5b1b6f7f40 NEWS --- a/NEWS Thu Mar 22 17:18:33 2018 +0100 +++ b/NEWS Fri Mar 23 10:52:00 2018 +0100 @@ -194,6 +194,9 @@ *** HOL *** +* Abstract bit operations as part of Main: push_bit, push_take, +push_drop. + * New, more general, axiomatization of complete_distrib_lattice. The former axioms: "sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)"