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