--- a/ProgTutorial/Intro.thy	Wed Apr 08 09:55:39 2009 +0200
+++ b/ProgTutorial/Intro.thy	Wed Apr 08 10:40:16 2009 +0100
@@ -60,13 +60,14 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  learn from it. The UNIX command @{text "grep -R"} is
-  often your best friend while programming with Isabelle. 
+  learn from it. The GNU/UNIX command @{text "grep -R"} is
+  often your best friend while programming with Isabelle, or
+  hypersearch if you use jEdit under MacOSX.
   \end{description}
 
 *}
 
-section {* Typographic Conventions *}
+section {* Typographic Conventions in the Tutorial *}
 
 text {*
 
@@ -116,7 +117,26 @@
   A few exercises are scattered around the text. Their solutions are given 
   in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
   to solve the exercises on your own, and then look at the solutions.
+*}
 
+section {* Naming Conventions in the Isabelle Sources *}
+
+text {*
+  There are a few naming conventions in Isabelle that might aid reading 
+  and writing code. (Remember that code is written once, but read numerous 
+  times.) The most important conventions are:
+
+  \begin{itemize}
+  \item @{text t}, @{text u} for (raw) terms, @{ML_type term}
+  \item @{text ct}, @{text cu} for certified terms, @{ML_type cterm}
+  \item @{text "ty"}, @{text T}, @{text U} for (raw) types, @{ML_type typ}
+  \item @{text th}, @{text thm} for theorems, @{ML_type thm}
+  \item @{text "foo_tac"} for tactics, @{ML_type tactic}
+  \item @{text thy} for theories, @{ML_type theory}
+  \item @{text ctxt} for proof contexts, @{ML_type Proof.context}
+  \item @{text lthy} for local theories, @{ML_type local_theory}
+  \item @{text context} for generic contextx, @{ML_type Context.generic}
+  \end{itemize}
 *}
 
 section {* Acknowledgements *}
@@ -152,6 +172,7 @@
   Please let me know of any omissions. Responsibility for any remaining
   errors lies with me.\bigskip
 
+  \vspace{5cm}
   {\Large\bf
   This document is still in the process of being written! All of the
   text is still under construction. Sections and 

Binary file progtutorial.pdf has changed