changeset 225 | 7859fc59249a |
parent 215 | 8d1a344a621e |
child 228 | fe45fbb111c5 |
--- 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