Re: [isabelle] locales, including documentation & possible programming bugs

On Fri, May 4, 2012 at 6:01 AM, Bill Richter
<richter at> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.