This sort of thing is well-known but very rare these days. I guess it could trap an unwary user. It just isn't easy to fix, given the old strategy of using assumptions, discarding them, and repeating. Larry
On 5 Aug 2010, at 06:33, John Matthews wrote: > Was it ever resolved whether auto should work this way? I'd always assumed > that "auto" was a safe tactic, provided I didn't try to spoof it by > pretending unsafe rules were safe, etc. > > I think most other Isabelle users also assume auto is safe. > > In any case, here is another example where auto turns a provable subgoal into > an unprovable one. This example doesn't require locales or the assumes..shows > form of a lemma statement: > > lemma > "ALL (x::nat). x = y ==> False" > apply (erule allE) > apply auto > > After the first step in the proof the subgoal remains provable, but then > after the call to auto the subgoal becomes False. _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
