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