578   @{text I}, @{text K}

   578   Perhaps one of the most puzzling aspects for a beginner when looking at 

   579   existing Isabelle code is the liberal use of combinators. At first they 

   580   seem to obstruct reading the code, but after getting familiar with them 

   581   they actually ease the reading and also the programming.

   582 

   583   \begin{readmore}

   584   The most frequently used combinator are defined in @{ML_file "Pure/library.ML"}

   585   and @{ML_file "Pure/General/basics.ML"}.

   586   \end{readmore}

   587 

   588   The simplest combinator is @{ML I} which is just the identidy function.

   589 *}

   590 

   591 ML{*fun I x = x*}

   592 

   593 text {*

   594   Another frequently used combinator is @{ML K}

   595