equal
deleted
inserted
replaced
5 header {* An experimental pattern-matching notation *} |
5 header {* An experimental pattern-matching notation *} |
6 |
6 |
7 theory Pattern_Match |
7 theory Pattern_Match |
8 imports HOLCF |
8 imports HOLCF |
9 begin |
9 begin |
|
10 |
|
11 default_sort pcpo |
10 |
12 |
11 text {* FIXME: Find a proper way to un-hide constants. *} |
13 text {* FIXME: Find a proper way to un-hide constants. *} |
12 |
14 |
13 abbreviation fail :: "'a match" |
15 abbreviation fail :: "'a match" |
14 where "fail \<equiv> Fixrec.fail" |
16 where "fail \<equiv> Fixrec.fail" |