| changeset 44898 | ec3f30b8c78c |
| parent 43976 | af17d7934116 |
| child 47232 | e2f0176149d0 |
| 44897:787983a08bfb | 44898:ec3f30b8c78c |
|---|---|
1 (* Author: Andreas Lochbihler, KIT *) |
1 (* Title: HOL/Library/Cset_Monad.thy |
2 Author: Andreas Lochbihler, Karlsruhe Institute of Technology |
|
3 *) |
|
2 |
4 |
3 header {* Add monad syntax for Csets *} |
5 header {* Monad notation for computable sets (cset) *} |
4 |
6 |
5 theory Cset_Monad |
7 theory Cset_Monad |
6 imports Cset Monad_Syntax |
8 imports Cset Monad_Syntax |
7 begin |
9 begin |
8 |
10 |