diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Intro.thy
--- a/CookBook/Intro.thy	Mon Jan 12 16:49:15 2009 +0000
+++ b/CookBook/Intro.thy	Wed Jan 14 16:46:07 2009 +0000
@@ -64,5 +64,12 @@
 
 *}
 
+section {* Conventions *}
+
+text {*
+  We use @{text "$"} to indicate a command needs to be run on the Unix-command
+  line.
+*}
+
 
 end
\ No newline at end of file