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
