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

[Makarius]

On Fri, 12 Sep 2008, Tobias Nipkow wrote:

> 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

It is a bit hard to follow this fragmentary stuff, nevertheless I managed 
to find the source of the presumed problem.

Concerning "my version", "your version" of the sources, we can do this 
properly once we have switched to Mercurial, because it provides unique 
version identifiers which other people can use to look up the very version 
precisely.


	Makarius