[isabelle-dev] Typerep again

[Florian Haftmann]

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

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090209/d5cbc169/attachment.sig>