# [isabelle] question on ISAR, printing theory file

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.

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