| changeset 49759 | ecf1d5d87e5e |
| parent 48891 | c0eafbd55de3 |
| child 58880 | 0baae4311a9f |
| 49758:718f10c8bbfc | 49759:ecf1d5d87e5e |
|---|---|
11 |
11 |
12 subsection {* Pattern-match monad *} |
12 subsection {* Pattern-match monad *} |
13 |
13 |
14 default_sort cpo |
14 default_sort cpo |
15 |
15 |
16 pcpodef (open) 'a match = "UNIV::(one ++ 'a u) set" |
16 pcpodef 'a match = "UNIV::(one ++ 'a u) set" |
17 by simp_all |
17 by simp_all |
18 |
18 |
19 definition |
19 definition |
20 fail :: "'a match" where |
20 fail :: "'a match" where |
21 "fail = Abs_match (sinl\<cdot>ONE)" |
21 "fail = Abs_match (sinl\<cdot>ONE)" |