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

[Tobias Nipkow]

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