Re: [isabelle] Several questions about coding style/best practices

I agree with Larry about brackets, but acknowledge that's personal preference. I know many people who prefer linear mode.

BTW the print mode is also accessible in jedits option menu, use plugins isabelle general options and look for the print mode field.


-------- Original Message --------
Subject: Re: [isabelle] Several questions about coding style/best practices
From: Lawrence Paulson <lp15 at>
To: mailing-list anonymous <mailing.list.anonymous at>
CC: cl-isabelle-users <cl-isabelle-users at>

I strongly prefer the bracketed style. The linear style is not very legible, especially when there is nesting.

But there are different points of view, and the bracket-style print mode is hard to access. To enable it, insert the line


in your settings file.

Larry Paulson

> On 7 Jul 2019, at 12:42, mailing-list anonymous wrote:
> I would like to clarify certain aspects related to the coding style best
> suited for Isabelle2019. The question combines both my concerns about the
> changes associated with the new release and, also, some of my previous
> concerns. Unfortunately, I was not able to find an explicit Isabelle coding
> style guide - please accept my apologies for asking this question if a
> document that answers it already exists somewhere.
> 1. Should ⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T) be preferred over S ⊆ 𝔘
> ⟹ T ⊆ 𝔘 ⟹ τ S ⟹ τ T ⟹ τ (S ∩ T)?
> 2. Should ['a set, ('a set ⇒ bool), 'a set] ⇒ bool be preferred over 'a set
> ⇒ ('a set ⇒ bool) ⇒ 'a set ⇒ bool?

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