diff -r bfcb8edbd851 -r e5990cd1b51a ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Jul 22 09:48:43 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Jul 22 09:53:35 2009 +0200
@@ -2027,7 +2027,7 @@
 100016, 100017, 100018, 100019, 100020"}
 
   where @{ML upto} generates a list of integers. You can print out this
-  list as an ``set'', that means enclosed inside @{text [quotes] "{"} and
+  list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
   @{text [quotes] "}"}, and separated by commas using the function
   @{ML [index] enum in Pretty}. For example
 *}