[isabelle] Using Nominal Isabelle in Isabelle2013/2014



Hi,

Is it recommended that one uses Nominal2 or the original Nominal package
with the latest version of Isabelle?  Nominal2 does not seem to have as
much documentation (or automation, from my brief attempt to use it), is
described as "alpha-ware" on the project website, and is not distributed
with the standard Isabelle distribution.

On the other hand, I'm trying to use the Nominal package as distributed in
Isabelle2014-RC1 and coming unstuck trying to define a function over a
nominal datatype using the "function" package that cannot be hammered into
a nominal_primrec easily, and having trouble closing the generated proof
obligations, with various exceptions being thrown by Isabelle (for example,
pat_completeness fails with a dest_eq exception).

So, now I'm wondering whether I'm doing something wrong, whether I've come
across a bug, or whether I'm just using software that is now deprecated
(the original Nominal package), and shouldn't be used with current versions
of the system.

Thanks,
Dominic



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