diff -r 73f716b9201a -r 95461cf6fd07 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Sun Dec 06 14:26:14 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Fri Jan 01 00:19:11 2010 +0100 @@ -406,10 +406,10 @@ section {* Combinators\label{sec:combinators} *} text {* - For beginners perhaps the most puzzling parts in the existing code of Isabelle are - the combinators. At first they seem to greatly obstruct the - comprehension of the code, but after getting familiar with them, they - actually ease the understanding and also the programming. + For beginners perhaps the most puzzling parts in the existing code of + Isabelle are the combinators. At first they seem to greatly obstruct the + comprehension of code, but after getting familiar with them and handled with + care, they actually ease the understanding and also the programming. The simplest combinator is @{ML_ind I in Library}, which is just the identity function defined as