Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] question on ISAR, printing theory file

view this post on Zulip Email Gateway (Aug 18 2022 at 10:37):

From: Revantha Ramanayake <revantha@rsise.anu.edu.au>
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.

Last updated: Nov 21 2024 at 12:39 UTC