# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1249455508 -7200
# Node ID 14173c0e8688e54dab8b0818b2fe48ccb59f172e
# Parent  05e6a33edef665cc5bd331ac6a2366ff60069da4
polished comment for error function

diff -r 05e6a33edef6 -r 14173c0e8688 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Aug 04 16:18:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 05 08:58:28 2009 +0200
@@ -165,6 +165,10 @@
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 
+  This function raises the exception @{text ERROR} which will then 
+  be displayed by the infrastructure.
+
+
   (FIXME Mention how to work with @{ML [index] debug in Toplevel} and 
   @{ML [index] profiling in Toplevel}.)
 *}
@@ -2257,7 +2261,7 @@
 
 ML {*Datatype.get_info @{theory} "List.list"*}
 
-section {* Name Space(TBD) *}
+section {* Name Space Issues (TBD) *}
 
 
 end
diff -r 05e6a33edef6 -r 14173c0e8688 progtutorial.pdf
Binary file progtutorial.pdf has changed