[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  
similar scheme?


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 MHonArc.