equal
deleted
inserted
replaced
31 |
31 |
32 (* deprecated, use thm with style instead, will be removed *) |
32 (* deprecated, use thm with style instead, will be removed *) |
33 (* aligning equations *) |
33 (* aligning equations *) |
34 notation (tab output) |
34 notation (tab output) |
35 "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and |
35 "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and |
36 "==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)") |
36 "Pure.eq" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)") |
37 |
37 |
38 (* Let *) |
38 (* Let *) |
39 translations |
39 translations |
40 "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)" |
40 "_bind (p, CONST DUMMY) e" <= "_bind p (CONST fst e)" |
41 "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)" |
41 "_bind (CONST DUMMY, p) e" <= "_bind p (CONST snd e)" |