Re: [isabelle] Question on Goal and on Use_thy. Thank you.

On Thu, 2 Dec 2010, olfa mraihi wrote:

1)As a first example on using Isabelle within ProofGeneral I've tried this simple one:   Goal "(2::nat)+2=4" by auto   but when I clicked on Use button in order to let Isabelle process it, I had an Outer syntax error:command expected! what's the problem?

Where did you see these examples? It must have been some really ancient manual -- some of them are distributed with the official release, but explicitly marked as "old" and "outdated".

2)does use_thy still available on Isabelle 2009?if not which command replace it?

use_thy still exists, although in practice you normally use the simultaneous version use_thys to exploit parallel loading. All of this only makes sense in batch sessions, i.e. in the ROOT.ML thereof.

In interaction with Proof General you just type your theory text and let the editor pass the commands to the prover.

See one of the newer manuals how this should look like.


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