| changeset 21210 | c17fd2df4e9e |
| parent 19674 | 22b635240905 |
| child 21404 | eb85850d3eb7 |
--- a/src/HOL/Library/OptionalSugar.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Library/OptionalSugar.thy Tue Nov 07 11:47:57 2006 +0100 @@ -17,7 +17,7 @@ (* aligning equations *) -const_syntax (tab output) +notation (tab output) "op =" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) "==" ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")