--- a/src/HOL/Library/LaTeXsugar.thy Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Thu Mar 05 08:23:11 2009 +0100
@@ -30,7 +30,7 @@
(* empty set *)
notation (latex)
- "{}" ("\<emptyset>")
+ "Set.empty" ("\<emptyset>")
(* insert *)
translations