equal
deleted
inserted
replaced
182 up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where |
182 up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" where |
183 "up_pat p = fup\<cdot>p" |
183 "up_pat p = fup\<cdot>p" |
184 |
184 |
185 definition |
185 definition |
186 TT_pat :: "(tr, unit) pat" where |
186 TT_pat :: "(tr, unit) pat" where |
187 "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail fi)" |
187 "TT_pat = (\<Lambda> b. If b then succeed\<cdot>() else fail)" |
188 |
188 |
189 definition |
189 definition |
190 FF_pat :: "(tr, unit) pat" where |
190 FF_pat :: "(tr, unit) pat" where |
191 "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>() fi)" |
191 "FF_pat = (\<Lambda> b. If b then fail else succeed\<cdot>())" |
192 |
192 |
193 definition |
193 definition |
194 ONE_pat :: "(one, unit) pat" where |
194 ONE_pat :: "(one, unit) pat" where |
195 "ONE_pat = (\<Lambda> ONE. succeed\<cdot>())" |
195 "ONE_pat = (\<Lambda> ONE. succeed\<cdot>())" |
196 |
196 |