*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Generating PDFs from .thy Files*From*: "Nauman ..." <recluze at gmail.com>*Date*: Fri, 8 Jun 2007 18:09:50 +0500

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 Hi. I have recently started to learn Isabelle/ISAR. I have the following questions: 1) The following is an extract from my theory file and partial output in ProofGeneral (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 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

- Previous by Date: Re: [isabelle] int vs. of_nat
- Next by Date: [isabelle] postdoctoral researcher position in Innsbruck
- Previous by Thread: Re: [isabelle] int vs. of_nat
- Next by Thread: [isabelle] postdoctoral researcher position in Innsbruck
- Cl-isabelle-users June 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list