[isabelle-dev] Common Names

[Tobias Nipkow]

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 
antiquotations.

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!
Tobias

PS Am in the process of hiding swap.