Re: [isabelle] Interpretation inside locale raises DUP



 On 25 November, 2013 21:57 CET, Makarius <makarius at sketis.net> wrote: 
 
> > Unfortunately, there is another locale bug, the diagnostic command 
> > 'print_interps <locale>' doesn't seem to work anymore either, but I 
> > haven't had time to look into that yet.
> 
> Do you have an example for that?  I did not find one looking 5min.

locale foo begin
print_interps foo
end

should yield 'foo' not 'no interpretations'.  Likewise

locale foo begin
interpretation foo .
print_interps foo
end

which is equivalent.  (In the language of locales, entering a context is making an interpretation via an identity morphism.)

> We need to figure it if and what to do here concerning the Isabelle2013-2 
> release, which is already the second attempt.  The release process needs 
> to terminate eventually.

I don't think this is a recent regression and suggest to ignore the problem for the upcoming release.

Clemens





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.