# HG changeset patch
# User nipkow
# Date 1106829201 -3600
# Node ID b8cb20cc0c0b6ed6528f1094bb825280c4227d08
# Parent  fdf9434b04ead626cabe1347edacdc8bf305dfba
fixed bugs

diff -r fdf9434b04ea -r b8cb20cc0c0b 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)
diff -r fdf9434b04ea -r b8cb20cc0c0b src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Thu Jan 27 12:37:02 2005 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Thu Jan 27 13:33:21 2005 +0100
@@ -3,7 +3,7 @@
     Author:     Gerwin Klain, Tobias Nipkow
     Copyright   2005 NICTA and TUM
 *)
-
+(*<*)
 theory OptionalSugar
 imports LaTeXsugar
 begin
@@ -34,4 +34,5 @@
   "_bind (DUMMY#p) e" <= "_bind p (tl e)"
 
 
-end
\ No newline at end of file
+end
+(*>*)