how to use this guide:
The idea of this project is to help users of Coq learn Isabelle and how to do simple metatheory using Isabelle/HOL. The format, as it stands, is that Isabelle code is interlaced with the original, commented out, coq code. My own comments are labled CH. Hopefully there will soon be a slightly more clean way of dealing with the interlacing and instructions for how to use that will be included later.