On 05.08.2010 07:33, John Matthews wrote:
lemma
ALL (x::nat). x = y == False
apply (erule allE)
After this step, the subgoal ?x = y == False remains, which cannot be
proven. Else, we could prove:
schematic_lemma foo: ?x = y == False
sorry
lemma False by (auto intro: foo[of 1 1,
Hi Lars,
You are mis-reading the schematic goal below:
lemma
ALL (x::nat). x = y == False
apply (erule allE)
After this step, the subgoal ?x = y == False remains, which cannot be
proven. Else, we could prove:
schematic_lemma foo: ?x = y == False
sorry
lemma False by (auto intro: foo[of
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
