added "set" supression
authornipkow
Sun May 06 13:33:39 2007 +0200 (2007-05-06)
changeset 2283537d3a984d730
parent 22834 bf67f798f063
child 22836 0e52bb862910
added "set" supression
src/HOL/Library/OptionalSugar.thy
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Sun May 06 13:33:01 2007 +0200
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Sun May 06 13:33:39 2007 +0200
     1.3 @@ -8,6 +8,10 @@
     1.4  imports LaTeXsugar
     1.5  begin
     1.6  
     1.7 +(* set *)
     1.8 +translations
     1.9 +  "xs" <= "set xs"
    1.10 +
    1.11  (* append *)
    1.12  syntax (latex output)
    1.13    "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)