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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
