Am Dienstag, den 05.07.2016, 20:02 +0200 schrieb Florian Haftmann:
>
> >
> >
> > What about adding it to the ab_group_add typeclass? I know this is
> > not
> > the usual mathematical syntax for permutations, but at least we can
> > reuse a lot of theorems from this type class.
> There *is* reuse
> What about adding it to the ab_group_add typeclass? I know this is not
> the usual mathematical syntax for permutations, but at least we can
> reuse a lot of theorems from this type class.
There *is* reuse since there is a separate interpretation of the
abstract ab_group locale.
I once met an a
What about adding it to the ab_group_add typeclass? I know this is not
the usual mathematical syntax for permutations, but at least we can
reuse a lot of theorems from this type class.
- Johannes
Am Dienstag, den 05.07.2016, 19:40 +0200 schrieb Florian Haftmann:
> >
> > One question: why did yo
Hello Andreas,
> AFAIU {.. deliver wrong positive.
> AFAIK the questionif 0 is part of natural numbers is disputed. Was there
> some solution in recent years?
> Depending on that {1..
> Cheers,
> Andreas
>
> On 05.07.2016 08:38, Tobias Nipkow wrote:
>> Florian,
>>
>> The whole setup has grown ov
Am 04.07.2016 um 23:49 schrieb Lars Hupel:
>> The problem I was referring to is that in order to get a deeper idea
>> what's going on you want to have a look at the topology of the history.
>> However I guess this is closely related to my surprise that not both
>> patches to distro and AFP pushed
> One question: why did you only set it up for monoid_mult and inverse,
> and not as a ab_group_mult?
The answer is simple: there is no type class ab_group_mult. Why? Since
our multiplicative structures are tailored towards rings where 0 is no
part of the multiplicative group.
Cheers,
F
Hi all,
after some more experiments, I found out that there is another difference
between explicit typeclass annotations and lemmas in the context: the former
theorems are included in instantiations but are not included in
interpretations. This usually does not make a difference, since there is
Ah sorry, my previous email should have been a response here.
Very nice!
One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?
- Johannes
Am Montag, den 04.07.2016, 21:25 +0200 schrieb Florian Haftmann:
> Hi all,
>
> see 59803048b0e8 for some
Very nice!
One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?
- Johannes
Am Montag, den 04.07.2016, 21:13 +0200 schrieb Florian Haftmann:
> Hi all,
>
> in 1a474286f315 I have introduced a locale for (total) bijections,
> allowing to obtain t
> On 5 Jul 2016, at 16:15, Lars Hupel wrote:
>
>> Another way of getting simultaneous tests would be to use subrepos. I.e.
>>
>> test-repo/
>> isabelle/ (subrepo)
>> afp/ (subrepo)
>>
>> The trigger would then be the push to test-repo, not to any of the subrepos,
>> and you would get a p
10 matches
Mail list logo
