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
> min :: "'a => 'a => 'a"
> 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