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



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






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