667 A more realistic example for this combinator is the following code |
667 A more realistic example for this combinator is the following code |
668 *} |
668 *} |
669 |
669 |
670 ML{*val (((one_def, two_def), three_def), ctxt') = |
670 ML{*val (((one_def, two_def), three_def), ctxt') = |
671 @{context} |
671 @{context} |
672 |> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"}) |
672 |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"}) |
673 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
673 ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"}) |
674 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*} |
674 ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*} |
675 |
675 |
676 text {* |
676 text {* |
677 where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"} |
677 where we make three definitions, namely @{term "One \<equiv> 1::nat"}, @{term "Two \<equiv> 2::nat"} |
678 and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial |
678 and @{term "Three \<equiv> 3::nat"}. The point of this code is that we augment the initial |
679 context with the definitions. The result we are interested in is the |
679 context with the definitions. The result we are interested in is the |
680 augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing |
680 augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing |
681 information about the definitions---the function @{ML_ind add_def in Local_Defs} returns |
681 information about the definitions---the function @{ML_ind add_def in Local_Defs} returns |
682 both as pairs. We can use this information for example to print out the definiens and |
682 both as pairs. We can use this information for example to print out the definiens and |
683 the theorem corresponding to the definitions. For example for the first definition: |
683 the theorem corresponding to the definitions. For example for the first definition: |