equal
deleted
inserted
replaced
570 ML %grayML{*fun double x = |
570 ML %grayML{*fun double x = |
571 x |> (fn x => (x, x)) |
571 x |> (fn x => (x, x)) |
572 |-> (fn x => fn y => x + y)*} |
572 |-> (fn x => fn y => x + y)*} |
573 |
573 |
574 text {* |
574 text {* |
575 The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your |
575 The combinator @{ML_ind ||>> in Basics} plays a central role whenever your |
576 task is to update a theory and the update also produces a side-result (for |
576 task is to update a theory and the update also produces a side-result (for |
577 example a theorem). Functions for such tasks return a pair whose second |
577 example a theorem). Functions for such tasks return a pair whose second |
578 component is the theory and the fist component is the side-result. Using |
578 component is the theory and the fist component is the side-result. Using |
579 @{ML ||>>}, you can do conveniently the update and also |
579 @{ML ||>>}, you can do conveniently the update and also |
580 accumulate the side-results. Consider the following simple function. |
580 accumulate the side-results. Consider the following simple function. |