# HG changeset patch
# User nipkow
# Date 1236945960 -3600
# Node ID 201887dcea0a619a10077a79d76282554cb2c9ab
# Parent  b80d2621caee675b39853262dd3d227b584b4572
added comment

diff -r b80d2621caee -r 201887dcea0a src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Fri Mar 13 12:32:29 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Fri Mar 13 13:06:00 2009 +0100
@@ -29,6 +29,7 @@
   "appendL (appendL xs ys) zs" <= "appendL xs (appendL ys zs)"
 
 
+(* deprecated, use thm_style instead, will be removed *)
 (* aligning equations *)
 notation (tab output)
   "op ="  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and