Re: [isabelle] New commands in Isabelle2012



Hi Dmitriy,

Thanks a lot! I updated the section accordingly
and also my own code in Nominal.

Thanks again,
Christian


On Sunday, June 17, 2012 at 08:03:49 (+0100), Dmitriy Traytel wrote:
 > 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.