src/HOL/Library/OptionalSugar.thy
changeset 22835 37d3a984d730
parent 21404 eb85850d3eb7
child 29494 a189c6274c7a
     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)