Re: [isabelle] New commands in Isabelle2012



Hi Christian,

one could also mention the @{command_spec foobar} antiquotation which allows you to avoid the duplication of the kind declaration in the code.

Best wishes,
Dmitriy

Am 17.06.2012 00:16, schrieb Christian Urban:
On Saturday, June 16, 2012 at 16:46:04 (+0100), Omar Montaño Rivas wrote:
  >  >
  >  >  If you use jEdit then the proof-script below will work. The
  >  >  difference is that the theory header now needs a declaration
  >  >  like
  >  >
  >  >    keywords "foobar" :: thy_decl
  >
  >  Yes, now it works in ProofGeneral. Thank you!
  >
  >  Omar.

I took the opportunity to update this section.
If you happen to have any feedback, I am grateful
to receive it.

Best wishes,
Christian






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