Email Gateway (Aug 18 2022 at 16:36): Email Gateway (Aug 18 2022 at 16:36):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 16:37):From: olfa mraihi <olfa.mraihi@yahoo.fr>
Hi Isabelle community,
I' m newbie on using Isabelle and I need you help by answering if possible these 2 first questions:
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?
2)does use_thy still available on Isabelle 2009?if not which command replace it?
Thank you very much.
Last updated: Apr 26 2024 at 04:17 UTC