equal
deleted
inserted
replaced
506 my_note @{binding "bar_conjunct2"} @{thm conjunct2} |
506 my_note @{binding "bar_conjunct2"} @{thm conjunct2} |
507 end *} |
507 end *} |
508 |
508 |
509 text {* |
509 text {* |
510 The function @{ML_text "my_note"} in line 3 is just a wrapper for the function |
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. |
511 @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory}; |
512 In lines 5 to 6 we call this function to give alternative names for three |
512 its purpose is to store a theorem under a name. |
513 theorems. The point of @{ML "#>"} is that you can sequence such functions. |
513 In lines 5 to 6 we call this function to give alternative names for the three |
|
514 theorems. The point of @{ML "#>"} is that you can sequence such function calls. |
514 |
515 |
515 The remaining combinators we describe in this section add convenience for |
516 The remaining combinators we describe in this section add convenience for |
516 the ``waterfall method'' of writing functions. The combinator @{ML_ind tap |
517 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 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 side-calculations or print out an intermediate result, for instance). The |