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