[isabelle] metis behaviour



Dear All,

I am trying to prove the following trivial first order theorem:

lemma "[|
ALL x y z.
   (X x | Y x | Z x | W x) &
   (X y | Y y | Z y | W y) & (X z | Y z | Z z | W z) -->
   R x y & R y z --> R x z;
R x y;
R y z;
X x;  X y; X z |]
==> R x z"
(* apply(metis) *)
apply(blast)
done

It works fine. But if I change blast to metis, the proof fails. Why?

Thanks

Tom





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