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

Makarius 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 mailing list