Re: [isabelle] overriding "min" syntax/constant notation

On Fri, 13 Mar 2009, Lucas Dixon wrote:

> I am wondering if it is possible to use the name "min", (and names of
> other constants defined by Isabelle) for my own constant without
> Isabelle writing my theory name in front of each occurrence...
> theory GreatBigLongTheoryName
> imports Main
> begin
> definition
>   min :: "'a => 'a => 'a"
> where
>   ...
> from now on goals with "min" get printed GreatBigLongTheoryName.min
> any suggestions?

You can globally disable the "unique_names" option of name spaces (either 
in Proof General or directly via ML).  An alternative is to tweak the 
theory context via ``hide (open) min'' etc. in your theory.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.