Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber: Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. CPP 2011: 183-198