*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] locales, including documentation & possible programming bugs*From*: Brian Huffman <huffman at in.tum.de>*Date*: Fri, 4 May 2012 08:06:48 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201205040401.q4441PxX003215@poisson.math.northwestern.edu>*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>

On Fri, May 4, 2012 at 6:01 AM, Bill Richter <richter at math.northwestern.edu> wrote: > My axiomatic geometry quest is now entirely about locales, and I have > a documentation bug. The syntax looks incorrect in both locales.pdf > and p 40 of the Isabelle/Isar Reference Manual, which has a nice group > theory example, from which I learned something about proofs. > > So I created the file Group1.thy below and had a lot of fun playing > with it in jedit. First notice all the "s and 's I inserted. There > are none of p 40, or in locales.pdf, and wouldn't that be great if we > didn't need them. I figured that out the `"'s & `''s easily by trial > and error, but It took me a long time to realize I had to put the > final period after the `"'. I agree that the omission of quotation marks in our pdf documentation is misleading and confusing, especially for new users who naturally want to copy examples manually from the pdf into their theory files. As a workaround, it may be useful to locate the source theories for the pdfs, and copy the definitions directly. (Look inside the doc-src directory in the distribution.) I can happily report that the new "Programming and Proving in Isabelle/HOL" tutorial in the upcoming Isabelle2012 release does show quotation marks in the examples. > I didn't know how to make the -1 exponent > in jedit, so I changed x^{-1} to sqrt x. Can someone tell me how? See appendix B of the Isabelle/Isar Reference Manual for a list of predefined symbols. > And here's another newbie question: If you have a 4-ary relation C, > how do you tell Isabelle you want to write it as a b <\equiv> c d? > That's what Tim does, but where is that explained? To introduce syntax like this, you will need to use the "notation" command with a mixfix declaration. (Search for "mixfix" in the Isabelle tutorial and old reference manual.) - Brian

**Follow-Ups**:**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Makarius

**Re: [isabelle] locales and proofs programming bugs***From:*Bill Richter

**Re: [isabelle] locales and proofs***From:*Bill Richter

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

**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

- Previous by Date: [isabelle] locales, including documentation & possible programming bugs
- Next by Date: Re: [isabelle] Isabelle2012-RC1 available for testing
- Previous by Thread: [isabelle] locales, including documentation & possible programming bugs
- Next by Thread: Re: [isabelle] locales, including documentation & possible programming bugs
- 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