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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
