[isabelle-dev] Typerep again

[Florian Haftmann]

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
>>>
>>

-- 

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/016553a4/attachment.sig>