On Thu, 18 Nov 2010, Brian Huffman wrote:
The effect of my change "typedef (open) unit" is to remove the
definition of the following constant
unit_def: "unit == {True}"
thus making the name "unit" available to users.
So this is a name space thing only? Maybe hide_const would do the job.
Historically, we could not hide it because it was "global", but Florian
has purged that recently.
Makarius
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
