src/HOL/Library/LaTeXsugar.thy

--- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 27 12:37:02 2005 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Jan 27 13:33:21 2005 +0100
@@ -32,6 +32,7 @@
 translations 
   "{x} \<union> A" <= "insert x A"
   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
+  "{x}" <= "{x} \<union> _emptyset"
 
 (* set comprehension *)
 syntax (latex output)