[isabelle-dev] Locale interpretation introduces abbreviations rather than definitions

[Makarius]

On Tue, 17 Jul 2012, Peter Lammich wrote:

> I have the problem that locale interpretation introduces abbreviations
> for locally defined constants, rather than definitions.

Cross-posting on isabelle-users and isabelle-dev is bad.

Since Florian has already answered on isabelle-users, the thread should be 
there exclusively (or a different one opened on isabelle-dev).


 	Makarius