added comment
authornipkow
Fri, 13 Mar 2009 13:06:00 +0100
changeset 30503 201887dcea0a
parent 30502 b80d2621caee
child 30504 b32d62c9c583
added comment
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