--- 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 *)