[isabelle-dev] class recpower and other classes...

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Nov 6 16:52:45 CET 2007


>>> The class recpower is very unfortunate. I suggest to remove it and
>>> replace it by definitions inside the locale/class (The axioms *are* a
>>> recursive function definition).

The class is surely an accident; however it has been there for 3 years
now.  We still have enough time after the Isabelle2007 release to fix
this.  (IMHO the key point is that we have to stop to abuse to type
system to achieve the same notation for different operations).

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20071106/96293e4e/attachment-0002.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20071106/96293e4e/attachment.sig>


More information about the isabelle-dev mailing list