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

Makarius makarius at sketis.net
Fri Jul 6 14:56:00 CEST 2012

On Tue, 3 Jul 2012, Lawrence Paulson wrote:

> Does anybody know (without going to the trouble of reproducing this 
> exact proof and obtaining a backtrace) why the function dest_equals is 
> being called on a sort constraint? At a guess, something is expecting a 
> definition.

Henri had put the SORT_CONSTRAINT in the 'where' part of 'interpretation' 
and that expects a proper equation at some point.  This is also explained 
in the manuals (isar-ref, locales).

The confusion was coming from 
where it looked like problem was solved.

In most practical situations, SORT_CONSTRAINT as it is now (Isabelle2012 
or today's Isabelle/3155cee13c49) works best in assumptions.


More information about the isabelle-dev mailing list