[isabelle-dev] Typerep again

[Amine Chaieb]

OK

Florian Haftmann wrote:
> I have to bother you further:
> 
> it is necessary to unfold the [HOL] node in the graph (by clicking on
> it) because we need to inspect the internal structure of the HOL theories.
> 
> 	Florian
> 
> Amine Chaieb schrieb:
>>
>> 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
>>>
>> ------------------------------------------------------------------------
>>
>> _______________________________________________
>> 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: permutations
Type: video/x-flv
Size: 7249 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090209/9148bfd9/attachment-0004.flv>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Misc
Type: video/x-flv
Size: 13180 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090209/9148bfd9/attachment-0005.flv>