*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Thu, 28 Feb 2013 10:59:44 +0100*In-reply-to*: <512E86E4.7040307@gmx.com>*References*: <512DD2E4.4070305@gmx.com> <512E2B19.8030705@gmx.com> <512E4902.2090507@gmx.com> <CAMej=25_=rN--ygVsqs390-Q-Suf8WC6US95oCJ8RgnycveJ-g@mail.gmail.com> <512E86E4.7040307@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.11) Gecko/20121122 Icedove/10.0.11

On 27.02.2013 23:21, Gottfried Barrow wrote:

(A = B) ====> (A seO B) --> (A = B), where "====>" means I have to convert (A=B) into the form (A seO B) before anything can be proved, and I can't get the simplifier to convert (A=B) to something like (A seO B), which I suppose is for good reason, since "=" is used everywhere. (In a manner of speaking, I manually convert (A=B) to (A seO B) as the first step in the proof.)

by (rule X) simp or, for a structured proof: proof (rule X) ... qed

-- Lars

**References**:**[isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

**Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

**Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

**Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Ramana Kumar

**Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Next by Date: [isabelle] two issues with Isabelle2013 on mac
- Previous by Thread: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Next by Thread: Re: [isabelle] Trying to reduce equality proofs from 2 to 1 step
- Cl-isabelle-users February 2013 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