[isabelle-dev] Typerep again
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
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)?
> 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
>>>> *** At command "theory".
>>> is it possible to make both Permutations and Misc to inherit from Main?
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev