--- 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)
--- 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
+(*>*)