See now 0a528e3aad28 and d3f4ddeaacc3 for the critical changes. Producing correct and readable patterns is a challenge and, unfortunately but necessarily, happens mostly without any backing from the inference kernel. Future work with more semantic foundations might bring progress here.
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
