[isabelle] overriding "min" syntax/constant notation



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?

cheers,
lucas

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






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