equal
deleted
inserted
replaced
18 bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54) |
18 bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54) |
19 |
19 |
20 notation (xsymbols) |
20 notation (xsymbols) |
21 bind (infixr "\<guillemotright>=" 54) |
21 bind (infixr "\<guillemotright>=" 54) |
22 |
22 |
|
23 notation (latex output) |
|
24 bind (infixr "\<bind>" 54) |
|
25 |
23 abbreviation (do_notation) |
26 abbreviation (do_notation) |
24 bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" |
27 bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" |
25 where |
28 where |
26 "bind_do \<equiv> bind" |
29 "bind_do \<equiv> bind" |
27 |
30 |
28 notation (output) |
31 notation (output) |
29 bind_do (infixr ">>=" 54) |
32 bind_do (infixr ">>=" 54) |
30 |
33 |
31 notation (xsymbols output) |
34 notation (xsymbols output) |
32 bind_do (infixr "\<guillemotright>=" 54) |
35 bind_do (infixr "\<guillemotright>=" 54) |
|
36 |
|
37 notation (latex output) |
|
38 bind_do (infixr "\<bind>" 54) |
33 |
39 |
34 nonterminals |
40 nonterminals |
35 do_binds do_bind |
41 do_binds do_bind |
36 |
42 |
37 syntax |
43 syntax |
44 "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54) |
50 "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54) |
45 |
51 |
46 syntax (xsymbols) |
52 syntax (xsymbols) |
47 "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13) |
53 "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13) |
48 "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54) |
54 "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54) |
|
55 |
|
56 syntax (latex output) |
|
57 "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54) |
49 |
58 |
50 translations |
59 translations |
51 "_do_block (_do_cons (_do_then t) (_do_final e))" |
60 "_do_block (_do_cons (_do_then t) (_do_final e))" |
52 == "CONST bind_do t (\<lambda>_. e)" |
61 == "CONST bind_do t (\<lambda>_. e)" |
53 "_do_block (_do_cons (_do_bind p t) (_do_final e))" |
62 "_do_block (_do_cons (_do_bind p t) (_do_final e))" |