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



Dear Joachim,

Thanks for the pointer to your development.  It looks like it will come in
useful.

Thanks,
Dominic


On 1 August 2014 11:40, Joachim Breitner <breitner at kit.edu> wrote:

> 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
>



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