equal
deleted
inserted
replaced
16 "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" |
16 "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)" |
17 |
17 |
18 |
18 |
19 (* aligning equations *) |
19 (* aligning equations *) |
20 notation (tab output) |
20 notation (tab output) |
21 "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) |
21 "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and |
22 "==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)") |
22 "==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)") |
23 |
23 |
24 (* Let *) |
24 (* Let *) |
25 translations |
25 translations |
26 "_bind (p,DUMMY) e" <= "_bind p (fst e)" |
26 "_bind (p,DUMMY) e" <= "_bind p (fst e)" |