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 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