--- a/ProgTutorial/FirstSteps.thy	Wed Jul 22 01:10:14 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Jul 22 08:46:54 2009 +0200
@@ -1551,8 +1551,9 @@
 ML{*val my_thms = ref ([] : thm list)*}
 
 text {* 
-  The purpose of this reference is that we are going to add and delete theorems
-  to the referenced list. However, a word of warning: such references must not 
+  The purpose of this reference is to store a list of theorems.
+  We are going to modify it by adding and deleting theorems.
+  However, a word of warning: such references must not 
   be used in any code that is meant to be more than just for testing purposes! 
   Here it is only used to illustrate matters. We will show later how to store 
   data properly without using references.

Binary file progtutorial.pdf has changed