[isabelle-dev] Common Names

Tobias Nipkow nipkow at in.tum.de
Fri May 30 18:31:12 CEST 2008

Dear theory developers,

 From time to time I find that somebody has added some function to 
HOL/Main that has a generic name (like `swap') but a fairly specific 
meaning (like "swap a b f = f(a := f b, b := f a)").

The disadvantage: since the name is common, it is likely that others 
have used it (or are going to), and they are suddenly confronted with 
qualified names MyTheory.swap through no fault of their own. It is not a 
disaster, but, for example, tends to mess up documentation produced by 

Could I urge everybody to
1. Consider carefully if such constants really needs to go into Main.
2. If they do, please hide the name:
    hide const swap
    It is still available in qualified form,
    but does not force new definitions of swap to be qualified.

What about uncommon names like `my_very_special_f'?
They should not be in Main to start with.

Thanks, and a wonderful summer w/e!

PS Am in the process of hiding swap.

More information about the isabelle-dev mailing list