| changeset 15140 | 322485b816ac |
| parent 14981 | e73f8140af78 |
| child 15236 | f289e8ba2bb3 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
1 (* Title: HOL/W0/W0.thy |
1 (* Title: HOL/W0/W0.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel |
3 Author: Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel |
4 *) |
4 *) |
5 |
5 |
6 theory W0 = Main: |
6 theory W0 |
7 imports Main |
|
8 begin |
|
7 |
9 |
8 section {* Universal error monad *} |
10 section {* Universal error monad *} |
9 |
11 |
10 datatype 'a maybe = Ok 'a | Fail |
12 datatype 'a maybe = Ok 'a | Fail |
11 |
13 |