*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] locales, including documentation & possible programming bugs*From*: Makarius <makarius at sketis.net>*Date*: Fri, 4 May 2012 12:20:17 +0200 (CEST)*In-reply-to*: <CAAMXsiaNt7gi9NPRAEAVvO4r8Mmor28YJprMrpkBBzUt9TUL=w@mail.gmail.com>*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>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 4 May 2012, Brian Huffman wrote:

I agree that the omission of quotation marks in our pdf documentation ismisleading and confusing, especially for new users who naturally want tocopy examples manually from the pdf into their theory files.

I can happily report that the new "Programming and Proving inIsabelle/HOL" tutorial in the upcoming Isabelle2012 release does showquotation marks in the examples.

Copy paste fails here, as anticipated. E.g. page 8, middle: fun app :: "′a list ⇒ ′a list ⇒ ′a list" where "app Nil ys = ys" | "app (Cons x xs) ys = Cons x (app xs ys)"

Makarius

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

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