Re: [isabelle] Proving relationships between locale predicates.

On Tue, 29 Nov 2011, Lars Noschinski wrote:

I only need one lemma from B, so I would really like to avoid instantiating A, as this takes very long (around 2.5s per instantiation).

I have recently started to make some more systematic performance measurements on the locale infrastructure. So if you can point me to the sources of a concrete example like yours above, the situation might eventually improve.


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