[isabelle-dev] Typerep again

Amine Chaieb ac638 at cam.ac.uk
Mon Feb 9 15:21:38 CET 2009

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 

The files are then under Multivariate.


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

More information about the isabelle-dev mailing list