Re: [isabelle] Modifying syntax of imported theories?



Regarding no_syntax and no_notation, they have the provoking property  
that it is hard to get the revoked syntax to stay revoked. If you  
unthinkingly include Set.thy, or anything else that directly imports  
Set.thy, all the ugly notation is right back where you don't want it.  
This means you frequently can't use the imports list that best  
describes or hints at the subject matter of a new theory. At least  
this was true in Isabelle 2005. Is it still true in the 2008 version?  
In the latest builds?

Perhaps rather than removing it from grammar it could be added to a  
deprecated production list or something?

Or else the theory import could be a bit smarter and not merge in a  
theory that is imported by another imported theory.

On 01/04/2009, at 7:34 PM, Peter Lammich wrote:

> Have you tried using the
>  no_notation
> declaration ?


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.