[isabelle-dev] Yet another encounter with HOL-Word
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev