isabelle: src/HOL/Library/Cset_Monad.thy@b7b905b23b2a (annotated)

44898 ec3f30b8c78c tuned bulwahn parents: 43976 diff changeset	1	(* Title: HOL/Library/Cset_Monad.thy
ec3f30b8c78c tuned bulwahn parents: 43976 diff changeset	2	Author: Andreas Lochbihler, Karlsruhe Institute of Technology
ec3f30b8c78c tuned bulwahn parents: 43976 diff changeset	3	*)
43976 af17d7934116 Add theory for setting up monad syntax for Cset Andreas Lochbihler parents: diff changeset	4
44898 ec3f30b8c78c tuned 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

author	haftmann
	Mon, 26 Dec 2011 22:17:10 +0100
changeset 45990	b7b905b23b2a
parent 44898	ec3f30b8c78c
child 47232	e2f0176149d0
permissions	-rw-r--r--