*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] locales, including documentation & possible programming bugs*From*: Bill Richter <richter at math.northwestern.edu>*Date*: Sun, 6 May 2012 18:30:53 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsiYY=TdfRVi5XiHAfcBAdZSZO1DQvQ_XqaGAwHTozisX+Q@mail.gmail.com> (message from Brian Huffman on Sun, 6 May 2012 07:32:04 +0200)*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205040401.q4441PxX003215@poisson.math.northwestern.edu> <CAAMXsiaNt7gi9NPRAEAVvO4r8Mmor28YJprMrpkBBzUt9TUL=w@mail.gmail.com> <201205052301.q45N1LWj018526@poisson.math.northwestern.edu> <CAAMXsiYY=TdfRVi5XiHAfcBAdZSZO1DQvQ_XqaGAwHTozisX+Q@mail.gmail.com>

Thanks, Brian, that's very helpful! I was really confused by the \equiv biz. Can you explain two more things: what do the 1000 priorities here even mean: [1000,1000,1000,1000] 70? If we right a b \cong c d, I want a & b to be bound really tightly together, so 1000 sounds like a good number, and I want the whole expression to be bound tighter than say and or implies, so 70 is a good number. But then I'd write it as [1000, 70, 1000]. Rules stated in terms of object logic connectives, like "P \<and> Q --> R", aren't very useful with the "rule" method. You had better state rules using "==>", like "P ==> Q ==> R" instead. I've been puzzled for some time by the preference (especially in Julien's Tarski geometry Coq code) by folks writing P ==> Q ==> R ==> S ==> T ==> U instead of the more sensible P & Q & R & S & T ==> U . And you're saying there's a good reason for this! Great! Can you explain why the first approach works better with rules? -- Best, Bill

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**[isabelle] locales, including documentation & possible programming bugs***From:*Bill Richter

**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Brian Huffman

**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Bill Richter

**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Brian Huffman

- Previous by Date: Re: [isabelle] locales, including documentation & possible programming bugs
- Next by Date: [isabelle] Proof help on Cardinality and list_all2
- Previous by Thread: Re: [isabelle] locales, including documentation & possible programming bugs
- Next by Thread: Re: [isabelle] Multi-dimensional arrays
- Cl-isabelle-users May 2012 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