402   For beginners perhaps the most puzzling parts in the existing code of Isabelle are

   402   For beginners perhaps the most puzzling parts in the existing code of Isabelle are

   403   the combinators. At first they seem to greatly obstruct the

   403   the combinators. At first they seem to greatly obstruct the

   404   comprehension of the code, but after getting familiar with them, they

   404   comprehension of the code, but after getting familiar with them, they

   405   actually ease the understanding and also the programming.

   405   actually ease the understanding and also the programming.

   406 

   406 

   408   identity function defined as

   408   identity function defined as

   409 *}

   409 *}

   410 

   410 

   411 ML{*fun I x = x*}

   411 ML{*fun I x = x*}

   412 

   412