*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] few questions about Isabelle/jEdit*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Sun, 20 Apr 2014 18:47:32 +0200*Organization*: Ada @ Home*References*: <CAGOKs0-ZoYyXJjm6xCGsarW+Avp86WUT+dfSKonUg+KCNoSWeg@mail.gmail.com>*User-agent*: Opera Mail/12.16 (Linux)

have tf3 : "(a-b)*(a-b)/2 + (a-c)*(a-c)/2 + (b-c)*(b-c)/2 = a*a + b*b + c*c - a*b - a*c - b*c" by algebra […]3. in the previous example, if I reverse the sides of the equality in"tf3"the "by algebra" part is colored red and the output buffer containssomered lines indicating failure. why does the order matter ?

The Find panel is a lot useful if you have a guess of what you need. -- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**References**:**[isabelle] few questions about Isabelle/jEdit***From:*noam neer

- Previous by Date: Re: [isabelle] few questions about Isabelle/jEdit
- Next by Date: [isabelle] jEdit UI: possibly confusing logic cessions list state
- Previous by Thread: Re: [isabelle] few questions about Isabelle/jEdit
- Next by Thread: [isabelle] jEdit UI: possibly confusing logic cessions list state
- Cl-isabelle-users April 2014 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