On 13/05/17 08:16, Florian Haftmann wrote:
>>> Are there good ideas how to do it with Binomial? Thus we could get rid
>>> of the Pre_Main theory from f533820e7248.
>>
>> The import could be changed e.g. to Groups_List.
>>
>> Desirable would also be to split the theory into Factorial and Binomial,
>> Are there good ideas how to do it with Binomial? Thus we could get rid
>> of the Pre_Main theory from f533820e7248.
>
> The import could be changed e.g. to Groups_List.
>
> Desirable would also be to split the theory into Factorial and Binomial,
> to raise awareness of existing combinatorial
Before I forget: I did that and it is as expected; everything still works.
Manuel
On 2017-04-25 11:12, Florian Haftmann wrote:
Am 25.04.2017 um 11:06 schrieb Manuel Eberl:
I think you actually solved that problem by now. If I recall correctly,
it was one of the two dictionary-related
Am 25.04.2017 um 11:06 schrieb Manuel Eberl:
> I think you actually solved that problem by now. If I recall correctly,
> it was one of the two dictionary-related problems I told you about a
> year ago or so, and then Lars and you solved that problem somehow.
>
> I can try putting in that code
I think you actually solved that problem by now. If I recall correctly,
it was one of the two dictionary-related problems I told you about a
year ago or so, and then Lars and you solved that problem somehow.
I can try putting in that code equation again and seeing what happens.
>> (*TODO: This
> * Theories "GCD" and "Binomial" are already included in "Main" (instead
> of "Complex_Main").
>
>
> This refers to Isabelle/f533820e7248: the change came up while exploring
> theory imports systematically. Normally, only "Main" or "Complex_Main"
> should be imported from the HOL session, not
