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


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

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


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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