Email Gateway (Aug 18 2022 at 10:34): Email Gateway (Aug 18 2022 at 10:34):From: Makarius <makarius@sketis.net>
On Wed, 6 Jun 2007, Revantha Ramanayake wrote:
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?
In order to finish the above goal, you may assume A and then have to show
"B --> C". The canonical structure of the text follows that of the
statements. Later on, things may be rearranged to improve the flow of
reasoning (e.g. drop unused assumptions, reorder assumptions).
2) Suppose my theory file is mydoc.thy. Because I am using ProofGeneral
the theory file is full of terms \<forall> \<exists> etc..
Try this to produce initial document setup (cf. the Isabelle System
manual):
isatool mkdir Test && isatool make
Alternatively, you may just invoke the Isabelle command 'display_drafts'
on the source files you wish to get pretty printed. (Proof General also
offers a menu item for that.)
Makarius
Last updated: May 03 2024 at 08:18 UTC