equal
deleted
inserted
replaced
54 former value should not be used again. To achieve this, |
54 former value should not be used again. To achieve this, |
55 we use a set of monad combinators: |
55 we use a set of monad combinators: |
56 *} |
56 *} |
57 |
57 |
58 notation fcomp (infixl "\<circ>>" 60) |
58 notation fcomp (infixl "\<circ>>" 60) |
59 notation (xsymbols) fcomp (infixl "\<circ>>" 60) |
59 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
60 notation scomp (infixl "o->" 60) |
|
61 notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60) |
|
62 |
60 |
63 abbreviation (input) |
61 abbreviation (input) |
64 "return \<equiv> Pair" |
62 "return \<equiv> Pair" |
65 |
63 |
66 text {* |
64 text {* |
110 Evaluation of monadic expressions by force: |
108 Evaluation of monadic expressions by force: |
111 *} |
109 *} |
112 |
110 |
113 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta |
111 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta |
114 |
112 |
|
113 |
|
114 subsection {* Do-syntax *} |
|
115 |
115 setup {* |
116 setup {* |
116 Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp} |
117 Adhoc_Overloading.add_variant @{const_name bind} @{const_name scomp} |
117 *} |
118 *} |
|
119 |
118 |
120 |
119 text {* |
121 text {* |
120 For an example, see HOL/Extraction/Higman.thy. |
122 For an example, see HOL/Extraction/Higman.thy. |
121 *} |
123 *} |
122 |
124 |