492   \isacommand{setup}-command. These functions have to be of type @{ML_type

   492   \isacommand{setup}- or \isacommand{local\_setup}-command. These functions 

   493   "theory -> theory"}. More than one such setup function can be composed with

   493   have to be of type @{ML_type "theory -> theory"}, respectively 

   494   @{ML "#>"}.\footnote{TBD: give example} 

   494   @{ML_type "local_theory -> local_theory"}. More than one such setup function 

   495   

   495   can be composed with @{ML "#>"}. Consider for example the following code, 

   496   The remaining combinators we describe in this section add convenience for the

   496   where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1} 

   497   ``waterfall method'' of writing functions. The combinator @{ML_ind tap in

   497   and @{thm [source] conjunct2} under alternative names.

   498   Basics} allows you to get hold of an intermediate result (to do some

   498 *}  

   499   side-calculations or print out an intermediate result, for instance). The function

   499 

   500 local_setup %graylinenos {* 

   501 let  

   502   fun my_note name thm = Local_Theory.note ((name, []), [thm]) #> snd

   503 in

   504   my_note @{binding "foo_conjI"} @{thm conjI} #>

   505   my_note @{binding "bar_conjunct1"} @{thm conjunct1} #>

   506   my_note @{binding "bar_conjunct2"} @{thm conjunct2}

   507 end *}

   508 

   509 text {*

   510   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 

   511   @{ML_ind note in Local_Theory}; its purpose is to store a theorem under a name. 

   512   In lines 5 to 6 we call this function to give alternative names for three

   513   theorems. The point of @{ML "#>"} is that you can sequence such functions. 

   514 

   515   The remaining combinators we describe in this section add convenience for

   516   the ``waterfall method'' of writing functions. The combinator @{ML_ind tap

   517   in Basics} allows you to get hold of an intermediate result (to do some

   518   side-calculations or print out an intermediate result, for instance). The

   519   function

   627   \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.}

   647   An example for this combinator is for example the following code

   628 *}

   648 *}

   649 

   650 ML {*

   651 val (((one_def, two_def), three_def), ctxt') = 

   652   @{context}

   653   |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) 

   654   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})

   655   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})

   656 *}

   657 

   658 ML {*

   659   @{context}

   660   |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) 

   661   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})

   662   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})

   663 *}

   664 

   665 ML {*

   666   val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) = 

   667   @{context}

   668   |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})

   669   ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})

   670   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})

   671 *}

   672