[isabelle] Generating PDFs from .thy Files

Date: Wed, 06 Jun 2007 03:39:28 +1000
From: Revantha Ramanayake <revantha at rsise.anu.edu.au >
Subject: [isabelle]  question on ISAR, printing theory file
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID: < 46659FD0.4090906 at rsise.anu.edu.au>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed


I have recently started to learn Isabelle/ISAR. I have the following

1) The following is an extract from my theory file and partial output in
(the lines in the script file have been prefixed by #):

#case A

goal (show, 1 subgoal)
1. A ==> B --> C

#assume "A"
#assume "B"
#show "U"

when I replace U with "C", "B --> C" or "B ==> B --> C" an error is
generated. What should
the form of U be in order to not generate an error?

2) Suppose my theory file is mydoc.thy. Because I am using ProofGeneral
the theory file is full of terms \<forall> \<exists> etc..

Is there a simple way of generating a dvi/pdf file to obtain a printable
version of my proof script with the proper symbols?

Thanks for any help.

Revantha Ramanayake.

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

I've written a small step-by-step howto on using "isatool make" -- isabelle
tool for generating PDFs. Take a look at it here:

Might I also interest you in a great Isabelle course offered at the
University of Insbruuk by Dr. Clemens Ballarin:
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

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