On Tue, Jul 17, 2012 at 11:04 AM, Christian Sternagel
c-ste...@jaist.ac.jp wrote:
Dear all,
I put together some functions on lists (that I use in some small proof) in
Data_List.thy. While doing so and thinking about functions and proofs I
would need in the future, I stumbled across the
Hi all,
I have the problem that locale interpretation introduces abbreviations
for locally defined constants, rather than definitions. This does not
work well with the code generator. Is there a way to make locale
interpretation introduce real definitions, and, if not, how much effort
would it
