2 imports Base

     2 imports Base

     3 begin

     3 begin

     4 

     4 

     5 

     5 

     6 chapter {* First Steps *}

     6 chapter {* First Steps *}

     8 

     7 

     9 text {* 

     8 text {* 

    10   Isabelle programming is done in Standard ML.

     9   Isabelle programming is done in Standard ML.

    11   Just like lemmas and proofs, code in Isabelle is part of a 

    10   Just like lemmas and proofs, code in Isabelle is part of a 

    12   theory. If you want to follow the code written in this chapter, we 

    11   theory. If you want to follow the code written in this chapter, we 

    48 @{ML_text "> true"}\smallskip

    47 @{ML_text "> true"}\smallskip

    49 

    48 

    50   then Isabelle's undo operation has no effect on the definition of 

    49   then Isabelle's undo operation has no effect on the definition of 

    51   @{ML_text "foo"}. Note that from now on we will drop the 

    50   @{ML_text "foo"}. Note that from now on we will drop the 

    52   \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever

    51   \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever

    54 

    53 

    55   Once a portion of code is relatively stable, one usually wants to 

    54   Once a portion of code is relatively stable, one usually wants to 

    56   export it to a separate ML-file. Such files can then be included in a 

    55   export it to a separate ML-file. Such files can then be included in a 

    57   theory by using \isacommand{uses} in the header of the theory, like

    56   theory by using \isacommand{uses} in the header of the theory, like

    58 

    57 

   570 fun ml_val_open (ys, []) txt = ml_val ys txt

   569 fun ml_val_open (ys, []) txt = ml_val ys txt

   571   | ml_val_open (ys, xs) txt =

   570   | ml_val_open (ys, xs) txt =

   572       ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");

   571       ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");

   573 

   572 

   574 fun ml_pat (rhs, pat) =

   573 fun ml_pat (rhs, pat) =

   576     (Symbol.explode pat))

   575     (Symbol.explode pat))

   577   in

   576   in

   578     "val " ^ pat' ^ " = " ^ rhs

   577     "val " ^ pat' ^ " = " ^ rhs

   579   end;

   578   end;

   580 

   579