Email Gateway (Aug 18 2022 at 10:34): Email Gateway (Aug 18 2022 at 10:34):From: "Nauman ..." <recluze@gmail.com>
Please refer to Chapter 4 of the Isabelle/HOL Tutorial. It has a nice
description of how to do this sort of thing. Indeed, this is a major plus
point of using Isabelle that you can create your proof documents very
easily.
I've written a small step-by-step howto on using "isatool make" -- isabelle
tool for generating PDFs. Take a look at it here:
http://recluze.wordpress.com/2007/06/07/pdfs-from-thy/
Might I also interest you in a great Isabelle course offered at the
University of Insbruuk by Dr. Clemens Ballarin:
http://cl-informatik.uibk.ac.at/teaching/ws06/atp/schedule.php
It has slides and exercices.
You would do great by going through the Isabelle/HOL tutorial and the course
before posting on the list. I know from experience. :)
Nauman ...
Blog: http://recluze.wordpress.com
Group: http://securityengineering.wordpress.com
Art gallery: http://recluse.gfxartist.com
Cell: 0321 90 66 275
Last updated: Nov 21 2024 at 12:39 UTC