# HG changeset patch
# User griff
# Date 1248245214 -7200
# Node ID 2927f205abba454b4165ce8c4b445f8fc9215d90
# Parent  c6b64fa9f301fd71737dd77d82ce5ca13594b417
reformulation

diff -r c6b64fa9f301 -r 2927f205abba ProgTutorial/FirstSteps.thy
--- 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.
diff -r c6b64fa9f301 -r 2927f205abba progtutorial.pdf
Binary file progtutorial.pdf has changed