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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
