[isabelle] Some comments on CONST/\<^const> mechanism in 2008
Sorry to be slow to the party, but the significance of the way the
definition/notation mechanism now works has only just started to sink
in. How do I find out more about it?
The mechanism seems to finally properly address the problem of
properly identifying and distinguishing constant and variables that
share names. This is really cool.
My question is as to how far this mechanism has penetrated the
pre-2008 world. It seems that datatype constructors are not included
in the new mechanism? Is there anyway include a const declared in the
old way, say because it is being defined by extension rather than
intension? Are type names included or planned for inclusion is a
IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.
This archive was generated by a fusion of
Pipermail (Mailman edition) and