Isabelle does not allow you to keep on proving a lemma after you have already proved all subgoals, although it could just ignore further proof steps, thus saving you the effort to comment them out...
Tobias Am 03/06/2012 21:29, schrieb Alexander Krauss: >> Thank you for investigating. I have been waiting for Alex to present his >> view. > > Sorry for being late. I've been offline for some days and am a bit behind now > :-) > >> Naturally, the current treatment resembles ML's. > > Yes. I don't think there were any further considerations. > > [...] >> There is no reason to allow a specification to contain material that may >> contradict another part of the specification. > > Well, the meaning of an equation in the "fun" command is: If the equation > overlaps with a previous one, consider just the non-overlapping part. And your > proposed change would be an exception to this rule. > > It does not happen very often, but I have occasionally written thing like this > myself in intermediate experimentation stages. Eventually, I clean things up > of > course, but having a hard error would force me to comment out more stuff > temporarily... > > But I understand your concerns. > > Technically, this situation represents a recoverable error (the definition and > the rest of the theory can be processed), but always indicates a problem in > the > sources that should be fixed. It seems that we do not currently have a > corresponding severity level. Therefore choosing between "ignored spam > warning" > and "break your leg error" is a bit difficult. > > Questions: > > - Do we need a level for such messages/annotations? In IDE terms, a little > yellow triangle with an exclamation mark comes to my mind. I wouldn't want to > see this for most iother warnings, but here it might make sense. > > - @Larry: Do you think your students would have noticed it if the redundant > equations had been underlined in yellow? > > - @Makarius: Is it already possible for a package to emit a message/report > that > carries position information, say to underline one of the clauses in a > specification processed by read_specification? This could also improve the > error > reporting in other cases. > > Alex > > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
