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
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-July/msg00003.html
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
