[isabelle] metis method and +-combinator
Hi all, I encounter the following problem with the metis-method and the
lemma "a#b ~= b" "a#b ~= b" "a#b ~= b" "a#b ~= a#x#b"
apply (metis not_Cons_self)+
The second apply-step will fail with the error message
*** Metis: No first-order proof with the lemmas supplied
*** At command "apply".
However, I would have expected the meaning of + to be: Apply argument
method(ical) repeatedly until it fails, at least once.
Hence "apply (metis not_Cons_self)+" should solve the first 3 subgoals.
This archive was generated by a fusion of
Pipermail (Mailman edition) and