Re: [isabelle] Weak lemmas in HOL-Analysis.Affine



I will take a look. Many thanks indeed for these! There must be hundreds more, so we need to keep looking.

Larry

> On 16 Oct 2020, at 15:07, Jakub Kądziołka <kuba at kadziolka.net> wrote:
> 
> I have encountered some weak theorems in HOL-Analysis.Affine, where a
> type is constrained to an euclidean space while any real vector space
> suffices. Please consider the following diff.





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