equal
deleted
inserted
replaced
15 "appendL xs ys" <= "xs @ ys" |
15 "appendL xs ys" <= "xs @ ys" |
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 const_syntax (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) |
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 |