| changeset 21404 | eb85850d3eb7 |
| parent 21210 | c17fd2df4e9e |
| child 22835 | 37d3a984d730 |
--- a/src/HOL/Library/OptionalSugar.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Library/OptionalSugar.thy Fri Nov 17 02:20:03 2006 +0100 @@ -18,7 +18,7 @@ (* aligning equations *) notation (tab output) - "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) + "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and "==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)") (* Let *)