[isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

> Cleaning up some obscure corners of the system, I've come across the old
> defer_recdef command.
> 
> Are there any remaining uses of this historical relic?  I don't see any
> in the main Isabelle repository + AFP.

Some years ago the idea was to let recdef stand as long as there are
examples in the distribution.  The consequence would be to dismantle
unused parts altogether.

Further suggestios?

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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