[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

[Lawrence Paulson]

I'm not sure that a warning is necessary. There were multiple factors in my confusion. 

One, clearly, was that type classes (like everything else) had always been global, and I never expected them to be localised. 

Two, I expected a type class such as complete_boolean_algebra to be canonical: the one defined in Main should be the right one, so any modification should be out of the question. 

I haven't actually studied the two definitions to see which one is really correct; getting these proofs working again is difficult enough. But either the one in Main needs to be corrected, or the local one needs to be given a more appropriate name.

Larry

On 22 Aug 2011, at 21:54, Makarius wrote:

> When I've seen the "complete_boolean_algebra" incident on the other thread my first impulse was to check how far the wiring of the class package wrt. the Isabelle document markup was.  In principle the prover can provide useful clues in non-intrusive ways here, if done right.  E.g. in Isabelle/jEdit one can hover over the text with COMMAND/CONTROL to ask "What is this?" and often get useful feedback already.
> 
> Unfortunately, the class package is still in a confusing state here, so I did not even put it on the list of things to be done, because it is just another instance of similar ongoing reforms, and there are so many really pressing things in the pipeline.  (Quite a bit has happened here already, like purging the name space module from historic cruft one more time, and assembling all syntax layers clearly in one place.)