author | bulwahn |
Tue, 10 Jan 2012 15:48:10 +0100 | |
changeset 46171 | 19f68d7671f0 |
parent 44898 | ec3f30b8c78c |
child 47232 | e2f0176149d0 |
permissions | -rw-r--r-- |
44898 | 1 |
(* Title: HOL/Library/Cset_Monad.thy |
2 |
Author: Andreas Lochbihler, Karlsruhe Institute of Technology |
|
3 |
*) |
|
43976
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
4 |
|
44898 | 5 |
header {* Monad notation for computable sets (cset) *} |
43976
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
6 |
|
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
7 |
theory Cset_Monad |
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
8 |
imports Cset Monad_Syntax |
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
9 |
begin |
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
10 |
|
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
11 |
setup {* |
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
12 |
Adhoc_Overloading.add_variant @{const_name bind} @{const_name Cset.bind} |
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
13 |
*} |
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
14 |
|
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff
changeset
|
15 |
end |