Jonathan P. Bowen, Mike Gordon: A shallow embedding of Z in HOL. Inf. Softw. Technol. 37(5-6): 269-276 (1995)