--- 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
--- 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)"