Re: [isabelle] Definition of fact

On Mon, 2 Nov 2015, Lawrence Paulson wrote:

I have noticed that sometimes when I prove a lemma involving type classes and tried to insert it next to similar lemmas, I get type-related error messages. I never quite grasped the unification of type classes with locales, and I have to say that while I use locales, I find our existing documentation very abstract and I hardly know whatâs going on sometimes.

(This is an underground part of the thread, resurfaced.)

Which documentation do you mean, "isar-ref" or "locales"? Things can be only improved when the authors of relevant sections know about it.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.