This is a collection of hints and conventions that enable you to write compilable and useful functions and formula faster. There are some obvious, syntactical issues but also more subtle things you should keep in mind when building a theory.

Some syntactical constructs of Isabelle/HOL are not as well-structures as you might think so you want to put parentheses around them. In particular, these applies to

• Conditions: (if P then x else y)
• Case distinctions: (case x of p1 ⇒ e1 | p2 ⇒ e2) * Constructors (in patterns): (x#xs) In all of these cases it is generally inadvisable to leave out the outermost parentheses. You might also often have to overwrite how Isabelle puts parentheses implicitly, for example around quantifiers: (ALL x. P x)''. If in doubt, check [Isabelle → Settings → Display → Show Brackets] and find out what exactly happens.