# HG changeset patch
# User nipkow
# Date 1178451219 -7200
# Node ID 37d3a984d73003dbbd2d5fa196a8be5173790942
# Parent  bf67f798f063ae73052da547fd3c8fae099d3867
added "set" supression

diff -r bf67f798f063 -r 37d3a984d730 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Sun May 06 13:33:01 2007 +0200
+++ b/src/HOL/Library/OptionalSugar.thy	Sun May 06 13:33:39 2007 +0200
@@ -8,6 +8,10 @@
 imports LaTeXsugar
 begin
 
+(* set *)
+translations
+  "xs" <= "set xs"
+
 (* append *)
 syntax (latex output)
   "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)