*To*: Joao Marcos <jmarcos at dimap.ufrn.br>*Subject*: Re: [isabelle] unexpected (for me) output using FOL*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 3 Nov 2006 09:37:54 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <a2727b60611021703m10b7e02fw1a97f5f900ef9ab2@mail.gmail.com>*References*: <a2727b60611021703m10b7e02fw1a97f5f900ef9ab2@mail.gmail.com>

Larry Paulson On 3 Nov 2006, at 01:03, Joao Marcos wrote:

(ALL x y. P(x, y)) <-> (ALL y x. P(x, y)) 1. ((ALL x. All(P(x))) --> (ALL y x. P(x, y))) & ((ALL y x. P(x, y)) --> (ALL x. All(P(x)))) val it = [] : Thm.thm list WHY does the system exchange some but not all instances of P(x,y) for P(x), and uses "All" to write the new goal?? I note that these things only occur when I use Goalw plus a rewrite rule such as iff_def, but not if I simply use Goal to prove my theorem. Why?

**References**:**[isabelle] unexpected (for me) output using FOL***From:*Joao Marcos

- Previous by Date: Re: [isabelle] unexpected (for me) output using FOL
- Next by Date: Re: [isabelle] Conditional interpretations?
- Previous by Thread: Re: [isabelle] unexpected (for me) output using FOL
- Next by Thread: [isabelle] Researcher position for two years
- Cl-isabelle-users November 2006 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