CookBook/Intro.thy
changeset 68 e7519207c2b7
parent 66 d563f8ff6aa0
child 75 f2dea0465bb4
--- 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