*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] overriding "min" syntax/constant notation*From*: Lucas Dixon <ldixon at inf.ed.ac.uk>*Date*: Fri, 13 Mar 2009 16:04:35 +0000*User-agent*: Thunderbird 2.0.0.19 (X11/20090107)

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.

**Follow-Ups**:**Re: [isabelle] overriding "min" syntax/constant notation***From:*Makarius

- Previous by Date: [isabelle] Call for paper - 10th Intl. Workshop on Termination - WST 2009
- Next by Date: Re: [isabelle] overriding "min" syntax/constant notation
- Previous by Thread: [isabelle] Call for paper - 10th Intl. Workshop on Termination - WST 2009
- Next by Thread: Re: [isabelle] overriding "min" syntax/constant notation
- Cl-isabelle-users March 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list