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



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.







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