[isabelle-dev] Specification packages in Isabelle/HOL, particularly primrec

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Jun 14 09:30:04 CEST 2019


(This thread is still open)

> Hence various *_global variants for specification packages have been
> removed.
> 
> What I have left untouched are the various variants of primrec. Is there
> still an ongoing work or plan to get rid of the old datatype / primrec
> layer, or at least to have that retreat further? Otherwise I would have
> a closer look a it to get an idea what can be done there.

The silence might indicate that there is actually no ongoing or planned
work.

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190614/66927527/attachment.sig>


More information about the isabelle-dev mailing list