On 07/17/2012 07:53 PM, Brian Huffman wrote:
2) I think at some point something like "set :: 'a list => 'a set" for HOLCF
lists would be useful...
What for? Is it meant to be an abstraction of some kind of executable
function, or is it only useful for writing logical specifications?
Only for s
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 sh
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 be
On Tue, Jul 17, 2012 at 11:04 AM, Christian Sternagel
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 following points:
>
>
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 following points:
1) how to name HOLCF functions for which similar functions already exi
