diff -r 647cab4a72c2 -r 7859fc59249a ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Wed Apr 01 15:42:47 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Thu Apr 02 11:48:35 2009 +0100 @@ -560,7 +560,7 @@ \begin{isabelle} \isacommand{thm}~@{text "TrueConj_def"}\\ - @{text "> "}@{thm TrueConj_def} + @{text "> "}~@{thm TrueConj_def} \end{isabelle} (FIXME give a better example why bindings are important; maybe