[isabelle] Z specifications in Isabelle

Hello all,

I am a PhD student looking at Z specifications and 
Isabelle and how the formalisation path can be broken down and 
simplified. I was wondering if anyone knows where I could find examples 
of full Z specifications and there proofs in isabelle, including all the
 .thy files needed?

Hope you can help

Thanks in advance

>From Lavinia

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.