src/HOL/Library/OptionalSugar.thy
changeset 38864 4abe644fcea5
parent 35250 92664dca6f20
child 42288 2074b31650e6
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  (* deprecated, use thm with style instead, will be removed *)
     1.5  (* aligning equations *)
     1.6  notation (tab output)
     1.7 -  "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
     1.8 +  "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
     1.9    "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
    1.10  
    1.11  (* Let *)