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

[Florian Haftmann]

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:
http://isabelle.in.tum.de/repos/isabelle/file/aa1acc25126b/src/HOL/Word/Misc_Typedef.thy,
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.

Cheers,
	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: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140228/baef6436/attachment-0001.asc>