Here’s the second presentation in the series. It deals with how HOL-Z can be used. It is only a skeletal presentation because honestly, you need to do a lot of reading before you can work with HOL-Z. This is just a rough guideline about the procedure followed. Here’s the link: