[isabelle-dev] Sort Annotation vs. Class Context for Lemmas

[Tjark Weber]

On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote:
> One issue can be that if some sort involves multiple type classes, the
> corresponding class may not have been defined. That is the one advantage
> of sorts: you can create conjunctions/intersection of type classes on
> the fly.

If there is just one intersection of type classes, one should perhaps
consider defining the corresponding class (before stating the lemma in
its context).  The alternative is that the poor user who later feels
that this class would be really useful has to re-prove every lemma.

Of course, this doesn't work for lemmas that involve separate sorts.

Kind regards,
Tjark