[isabelle-dev] Locale interpretation introduces abbreviations rather than definitions
makarius at sketis.net
Tue Jul 17 19:12:19 CEST 2012
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).
More information about the isabelle-dev