*To*: clefort <ipub at charter.net>*Subject*: Re: [isabelle] trivial proof to solve*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Fri, 12 Jan 2007 17:28:47 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <19460EC2-DDF2-4FB6-8A44-578566CCA8F9@charter.net>*References*: <19460EC2-DDF2-4FB6-8A44-578566CCA8F9@charter.net>*User-agent*: KMail/1.8

Clint, On Thursday 11 January 2007 16:55, clefort wrote: > theory trivial = Main: > > lemma "\<forall>x. \<forall>y. \<forall>z. EQ(F(x,y),S(y,z),EQ(y,x)) > \<and> EQ(HS(z,x),F(x,z),S(z,y)) > \<Longrightarrow> \<forall>x. \<forall>y. > \<forall>z. EQ(S(y,y),F(x,x),HS(z,z))" are you using Isabelle/HOL? I am getting a type error when I try to input this formula. Are F, S, HS, and EQ defined constants, or just uninterpreted functions? Best, Tjark

**References**:**[isabelle] trivial proof to solve***From:*clefort

- Previous by Date: [isabelle] Questios about evaluation and code extraction
- Next by Date: Re: [isabelle] trivial proof to solve/reply
- Previous by Thread: [isabelle] trivial proof to solve
- Next by Thread: Re: [isabelle] trivial proof to solve/reply
- Cl-isabelle-users January 2007 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