The oz2z program is rather flaky. It works well for straight-forward LaTeX files, but tends to get rather flustered for anything fancy. In particular, it won't recognise a Z paragraph if it is inside a macro argument. (A Z environment inside another environment is OK.) The whole thing needs re-writing. In the long term, it is intended that vimes include a theorem prover and proof checker.