Re: [isabelle] Nominal2 fails on Datatypes with Lists

Hi, Christian!

So did I get this correctly that Nominal2 isn’t further developed

By the way, is the restriction that values of a nominal data type may
not contain functions also in place in Nominal2?

All the best,

Am Donnerstag, den 17.10.2019, 12:35 +0000 schrieb Urban, Christian:
> Hi Wolfgang,
> Is Nominal2 somehow production-ready?
> This depends on your point of view. ;o) It is certainly true that it
> quite rough and not all features are implemented. And it was aeons ago
> I have done things with it. But at the same time people have found it
> useful and have used it in interesting formalisations, for example
> It really depends on what your point of view is and what you want to
> do.
> Christian
> ________________________________
> From: cl-isabelle-users-bounces at <
> cl-isabelle-users-bounces at> on behalf of Wolfgang
> Jeltsch <wolfgang-it at>
> Sent: 16 October 2019 22:04
> To: cl-isabelle-users at <
> cl-isabelle-users at>
> Subject: Re: [isabelle] Nominal2 fails on Datatypes with Lists
> Hi, Christian!
> Is Nominal2 somehow production-ready? From its website I got the
> impression that it had been developed only half-way and then
> development had halted.
> All the best,
> Wolfgang

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