diff -r d144fc51fe04 -r 96d10631eec2 ProgTutorial/Parsing.thy --- 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}