[isabelle] metis method and +-combinator



Hi all, I encounter the following problem with the metis-method and the +-combinator:

 lemma "a#b ~= b" "a#b ~= b" "a#b ~= b" "a#b ~= a#x#b"
   apply -
   apply (metis not_Cons_self)+
   apply (auto)


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.

Regards,
 Peter






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.