[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses
makarius at sketis.net
Fri Jul 6 15:56:46 CEST 2012
On the sister thread
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?
More information about the isabelle-dev