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
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