Re: [isabelle] Using Nominal Isabelle in Isabelle2013/2014



Hi,


Am Freitag, den 01.08.2014, 10:31 +0100 schrieb Dominic Mulligan:
> Thanks for your speedy reply.  I'll try and convert my development to
> Nominal2 in that case.  Is there any sort of manual or user guide on using
> the new package?  From my brief browsing of the examples supplied the
> amount of work one needs to do to define functions in Nominal2 is
> significantly higher than in Nominal1---is there any guidance on the new
> tactics/theorems supplied to help close these obligations?

not sure if they are helpful, but “real world examples” from someone not
developing Nominal2 can be found at
http://darcs.nomeata.de/isa-launchbury/Launchbury/

In particular after having defined a few functions over my expr type
defined in Terms.thy, I created a lemma (eqvt_lam_case and
eqvt_let_case, also in Terms.thy) that included all the boring stuff and
reduced the number of variables I have to talk about. I ugess it is my
own variant of the _FCB lemmas (which I didn’t figure out how to use
succesfully).

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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