*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] metis behaviour*From*: Tom Ridge <tjr22 at cam.ac.uk>*Date*: Fri, 04 Apr 2008 17:00:05 +0100*User-agent*: Thunderbird 2.0.0.12 (X11/20080226)

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

**Follow-Ups**:**Re: [isabelle] metis behaviour***From:*Lawrence Paulson

- Previous by Date: [isabelle] LFMTP'08: 2nd Call for Papers
- Next by Date: Re: [isabelle] Congruence rules for modular arithmetic
- Previous by Thread: [isabelle] LFMTP'08: 2nd Call for Papers
- Next by Thread: Re: [isabelle] metis behaviour
- Cl-isabelle-users April 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list