[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name
brianh at cs.pdx.edu
Mon Aug 22 17:17:49 CEST 2011
Isabelle prints out warning messages whenever anyone declares a
duplicate simp rule, intro rule, etc. It would be nice if Isabelle
would print a similar warning whenever a definition reuses a name that
is already in scope in the current context. For example, if a theory
defines a class like this...
class complete_boolean_algebra = distributive_complete_lattice + boolean_algebra
...and a class called "complete_boolean_algebra" is already in scope,
then a warning message ought to be printed.
Such a warning message would be useful for constant names, lemma
names, etc. as well.
More information about the isabelle-dev