--- 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