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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
