--- a/ProgTutorial/Parsing.thy Sat Dec 01 16:50:46 2012 +0000
+++ b/ProgTutorial/Parsing.thy Mon Dec 31 20:20:55 2012 +0000
@@ -12,6 +12,14 @@
Tony Travis in an email about the\\ ``LINUX is obsolete'' debate
\end{flushright}
+ \begin{flushright}
+ {\em
+ Document your code as if someone else might have to take it over at any
+ moment and know what to do with it. That person might actually be you --
+ how often have you had to revisit your own code and thought to yourself,
+ what was I trying to do here?} \\[1ex]
+ Phil Chu in ``Seven Habits of Highly Effective Programmers''
+ \end{flushright}
Isabelle distinguishes between \emph{outer} and \emph{inner}
syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}