src/HOLCF/Fixrec.thy
changeset 18096 574aa0487069
parent 18094 404f298220af
child 18097 d196d84c306f
     1.1 --- a/src/HOLCF/Fixrec.thy	Sun Nov 06 00:22:03 2005 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sun Nov 06 00:35:24 2005 +0100
     1.3 @@ -33,15 +33,10 @@
     1.4  
     1.5  subsection {* Monadic bind operator *}
     1.6  
     1.7 -constdefs
     1.8 -  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe"
     1.9 -  "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
    1.10 -
    1.11 -syntax
    1.12 -  "_bind" :: "'a maybe \<Rightarrow> ('a \<rightarrow> 'b maybe) \<Rightarrow> 'b maybe"
    1.13 -    ("(_ >>= _)" [50, 51] 50)
    1.14 -
    1.15 -translations "m >>= k" == "bind\<cdot>m\<cdot>k"
    1.16 +consts
    1.17 +  bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" (infixl ">>=" 50)
    1.18 +defs
    1.19 +  bind_def: "bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m"
    1.20  
    1.21  nonterminals
    1.22    maybebind maybebinds
    1.23 @@ -95,12 +90,10 @@
    1.24  
    1.25  subsection {* Monad plus operator *}
    1.26  
    1.27 -constdefs
    1.28 -  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe"
    1.29 -  "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
    1.30 -
    1.31 -syntax "+++" :: "'a maybe \<Rightarrow> 'a maybe \<Rightarrow> 'a maybe" (infixr 65)
    1.32 -translations "x +++ y" == "mplus\<cdot>x\<cdot>y"
    1.33 +consts
    1.34 +  mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" (infixr "+++" 65)
    1.35 +defs
    1.36 +  mplus_def: "mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1"
    1.37  
    1.38  text {* rewrite rules for mplus *}
    1.39