[isabelle] Isar Proof



lemma 
"[| ALL x . (P (x::'a)  =>  ~ Q x)  /\
                (P x        => ~ R x) /\
               (Q x       =>  ~ R x);
 EX x .  P x;
 EX x .  Q x;
 EX x .  R x|] ==>
EX  x y z. (~((x::'a) = y)  /\
          ~( x      = z)  /\
          ~( y      = z))"
  apply(elim ex_forward)
  apply(auto)
done
  

Can someone suggest an Isar equivalent for the above proof?
Thanks,
Tim




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