On Thu, 18 Nov 2010, Brian Huffman wrote:
On Thu, Nov 18, 2010 at 2:59 PM, Makarius <[email protected]> wrote:
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.
If you think it is useful to have Isabelle/HOL provide a constant
Product_Type.unit == {True}, then by all means put it back in.
I don't know if that is useful.
The point here is that formally it is a non-conservative change deep down
in the guts of HOL. Such things routinely cause surprises much later.
This means there must be a good reasong for the change -- a documented one
so others have a chance to review it quickly, without a long and tedious
thread on the mailing list.
Makarius_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
