HOL-Z is a proof environment for Z built as plug-in of the generic theorem prover Isabelle/HOL (Version 2005). It allows for importing Z specifications written in LaTeX and type-checked by the Java-based ZeTa-System. HOL-Z then allows for the formal analysis of such specifications, i.e. by - proving the conjectures stated in the specfication, - generating proof obligations concerning the consistency of state and operation schemas as well as their proof, and - generating proof obligations resulting from refinement statements for functional and data refinement.