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