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
