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

Brian Huffman brianh at cs.pdx.edu
Mon Aug 22 17:17:49 CEST 2011

Hello everyone,

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.

- Brian

More information about the isabelle-dev mailing list