[isabelle-dev] Typerep again

[Amine Chaieb]

Do you mean thy_deps? It's not working on my machine.
Can you do

cvs -d 
haftmann at cvsbroy.informatik.tu-muenchen.de:/usr/wiss/chaieb/.repos co 
work/Lib

The files are then under Multivariate.

Amine.

PS: Please forgive for still using cvs, but I am applying the first 
commandment of Computer science.

Florian Haftmann wrote:
> Can you provide me with a theory graph of Permutations and Misc?  (Isar
> command "thy_graph", export to ps/pdf)?
> 
> 	Florian
> 
> Amine Chaieb schrieb:
>> I've moved things up (although this is really artificial).
>>
>> Misc imports Complex_Main anyway, and I made Permutations import Main,
>> the problem persists.
>>
>>
>>
>> Florian Haftmann wrote:
>>> Hi Amine,
>>>
>>>> I have a theory development which used to work not a long time ago. I am
>>>> now trying to include it into the distribution.
>>>>
>>>> At some point I can not merge the theories and get:
>>>>
>>>> *** Clash of specifications "Permutations.typerep_^_inst.typerep_^_def"
>>>> and "Misc.typerep_^_inst.typerep_^_def" for constant
>>>> "Typerep.typerep_class.typerep"
>>>> *** At command "theory".
>>> is it possible to make both Permutations and Misc to inherit from Main?
>>>
>>>     Florian
>>>
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>