I'm only talking about cases where “show" must inevitably fail. Fortunately, such situations are rare, but if they can easily be detected, they should be. Larry
On 5 Sep 2012, at 14:20, Lars Noschinski <[email protected]> wrote: > On 05.09.2012 15:13, Lawrence Paulson wrote: >> Fixing a variable that ought to be free is an error. >> >> Highlighting is useful, but you have to be quite alert to notice it. I >> seldom notice it except in really blatant situations, like the same variable >> highlighted in two different ways. If the context is simply wrong, the >> highlighting should be absolutely unmissable. > > Indeed, a variable shadowed by mistake is quite hard to detect. But is there > a clear rule whether a variable "ought to be free"? Shadowing has its > legitimate use cases (e.g. I usually shadow the "n" in induction proofs on > the naturals). > > -- Lars _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
