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.


> On 16 Oct 2020, at 15:07, Jakub Kądziołka <kuba at> 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.