[isabelle-dev] [Fwd: Re: Find]

[Tobias Nipkow]

PS Ja, Gerwin hat recht, der Theoriename ist hilfreich.

Tobias Nipkow schrieb:
> Vermutlich spricht der "Optimierer" Deutsch und hat das in der letzten
> Woche "optmiert" - in der Version auf meinem Mac kommt auch noch der
> volle Name raus. Ideal waere die kuerzeste legale Abk.
> 
> Tobias
> -------- Original-Nachricht --------
> Betreff: Re: Find
> Datum: Fri, 12 Sep 2008 09:39:21 +1000
> Von: Gerwin Klein <gerwin.klein at nicta.com.au>
> An: Tobias Nipkow <nipkow at in.tum.de>
> Referenzen: <48C92DF8.7000903 at in.tum.de>
> 
> Wir sind unschuldig, das muß jemand "optimiert" haben. In unserer
> Version kommt immer der fully qualified name raus. Selbst wenn der
> kurze Name eindeutig ist, will man oft den langen, um rauszufinden aus
> welcher Theorie das Theorem kommt.
> 
> Gerwin
> 
> 
> 
> On 12/09/2008, at 0:40, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
>> gibt nur den Basisnamen eines Theorems aus. Das kann Probleme machen.
>> Such mal nach "fold _ _ _ (insert _ _)", dann bekommst du 3 mal
>> fold_insert, wobei das erste davon nur als  
>> ab_semigroup_mult.fold_insert
>> ansprechbar ist. Mit der richtigen name space function muesste da der
>> passend abgekuerzte Name rauskommen.
>>
>> Tobias
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev