Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Cset_Monad.thy
author wenzelm
Wed, 11 Jan 2012 21:04:22 +0100
changeset 46190 a42c5f23109f
parent 44898 ec3f30b8c78c
child 47232 e2f0176149d0
permissions -rw-r--r--
more conventional eval_tac vs. method_setup "eval"; clarified method "normalization": THEN_ALL_NEW avoids bumping into other subgoals;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44898
bulwahn
parents: 43976
diff changeset 
     1
 
(* Title: HOL/Library/Cset_Monad.thy
bulwahn
parents: 43976
diff changeset 
     2
 
   Author: Andreas Lochbihler, Karlsruhe Institute of Technology
bulwahn
parents: 43976
diff changeset 
     3
 
*)
43976
af17d7934116 Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
diff changeset 
     4
 







44898





bulwahn


parents: 
43976

diff
changeset




     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














isabelle