Re: [isabelle] Isabelle style guide - Part 2
On Sat, 30 May 2015, Gerwin Klein wrote:
As promised, part 2 of the Isabelle style guide:
Feedback for the first part was great, keep it coming!
* "Isabelle supports literal proofs": you probably mean "literate proofs".
This should give most people an idea about the point of it, although the
official slogan talks about "proof documents".
You could also add a note that the SideKick plugin of Isabelle/jEdit
helps getting an overview of a text that is nicely structured with
chapter, section, subsection etc.
* CamelCaseNames for datatype constructors: around 2006/2007 this was
discontinued as canonical form in Isabelle/Pure/ML and replaced by
Camel_Case_Names with_proper_underscore. Both the old and new forms are
widely used, though, since renaming constructors in ML is always a bit
dangerous (but not in HOL).
* About bad "definition f" and "This will reserve the name f and make it
unusable for variables". Having a constant called "f" in the global
context is certainly bad, but there should always be a way to produce a
free variable of that name, by using explicit "fixes", "for" or "!!f.
..." in closed propositions. Isar has been designed like that from the
very start, although surprisingly many people don't know that --
especially when building tools that ignore the concepts of
eigen-contexts of statements.
* "typed as \open and \close in jEdit": This should be Isabelle/jEdit,
since jEdit does not know anything about it. The canonical shortcut in
the Prover IDE works via ASCII backquote, although that is sometimes
hard to find on strange keyboards (e.g. German Macintosh). At some
point, the canonical key for cartouches might become " (double-quote),
when terms are accepted in that form as well.
This archive was generated by a fusion of
Pipermail (Mailman edition) and