[isabelle-dev] Typerep again

[Amine Chaieb]

Florian Haftmann wrote:
> Amine Chaieb schrieb:
>> Do you mean thy_deps? It's not working on my machine.
> 
> Yes, thy_deps of course (sorry for the slip).  But thy doesn't it work?
> 
> 	cd lib/browser
>         make
> 
> should do the job...
> 
> 	Florian
> 
>> 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
>>>>
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Misc
Type: video/x-flv
Size: 915 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090209/7edfb161/attachment-0004.flv>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: permutations
Type: video/x-flv
Size: 716 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090209/7edfb161/attachment-0005.flv>