[isabelle-dev] Fwd: [isabelle] Pending sort hypotheses

Makarius 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 mailing list