1 theory First_Steps

     1 theory First_Steps

     2 imports Base

     2 imports Base

     3 begin

     3 begin

     4                                                   

     4                                                   

     5 chapter \<open>First Steps\label{chp:firststeps}\<close>

     5 chapter \<open>First Steps\label{chp:firststeps}\<close>

     7 

     6 

     8 

     7 

     9 text \<open>

     8 text \<open>

    10   \begin{flushright}

     9   \begin{flushright}

    11   {\em ``The most effective debugging tool is still careful thought,\\ 

    10   {\em ``The most effective debugging tool is still careful thought,\\ 

   102   This function expects a string as argument. If you develop under

   101   This function expects a string as argument. If you develop under

   103   PolyML, then there is a convenient, though again ``quick-and-dirty'', method

   102   PolyML, then there is a convenient, though again ``quick-and-dirty'', method

   104   for converting values into strings, namely the antiquotation 

   103   for converting values into strings, namely the antiquotation 

   105   \<open>@{make_string}\<close>:

   104   \<open>@{make_string}\<close>:

   106 

   105 

   108 

   107 

   109   However, \<open>@{make_string}\<close> only works if the type of what

   108   However, \<open>@{make_string}\<close> only works if the type of what

   110   is converted is monomorphic and not a function. 

   109   is converted is monomorphic and not a function. 

   111 

   110 

   112   You can print out error messages with the function @{ML_ind error in Library}; 

   111   You can print out error messages with the function @{ML_ind error in Library};