[isabelle-dev] Yet another encounter with HOL-Word

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Feb 28 23:00:52 CET 2014

The carneval season is a good opportunity to have a look at well-known
dark matter parts of Isabelle, e.g. the theories in src/HOL/Word.
I particularly stumbled over this:
which creates some kind of psychodelic feelings when studying it. If it
was a front-loading washer, the manufacturer's guarantee would
definitely end when incorporating something like that, e.g. changing the
default declarations of typedef etc. And each application based on
HOL-Word is tainted with that!

I have the strong impression that the now existing infrastructure of
quotient relations, transfer etc. would form a much more solid base than
this adventurous low-level hacking. But someone would have to take the
burden and start to sort this out step by step.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140228/baef6436/attachment-0001.asc>

More information about the isabelle-dev mailing list