diff -r 32b4d3704415 -r bfcb8edbd851 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Wed Jul 22 09:21:21 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Wed Jul 22 09:48:43 2009 +0200 @@ -1943,7 +1943,7 @@ ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*} text {* - We deliberately chose a large string so that is spans over more than one line. + We deliberately chose a large string so that it spans over more than one line. If we print out the string using the usual ``quick-and-dirty'' method, then we obtain the ugly output: