On the sister thread
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-July/msg00028.html
Henri mentions finite_UNIV.
Trying to reproduce the observed effects with Isabelle2012 vs.
Isabelle/3155cee13c49 from today reveals a difference wrt. Phantom('a).
The latter was introduced in Isabelle/f0ecc1550998 with an almost vacous
log entry, and no coverage in NEWS nor CONTRIBUTORS.
What is its purpose? Where is it documented?
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
