src/HOL/Library/LaTeXsugar.thy
changeset 27688 397de75836a1
parent 27487 c8a6ce181805
child 29493 ddcbd5e4041d
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sun Jul 27 20:08:16 2008 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon Jul 28 20:49:07 2008 +0200
     1.3 @@ -30,17 +30,15 @@
     1.4  (* SETS *)
     1.5  
     1.6  (* empty set *)
     1.7 -syntax (latex output)
     1.8 -  "_emptyset" :: "'a set"              ("\<emptyset>")
     1.9 -translations
    1.10 -  "_emptyset"      <= "{}"
    1.11 +notation (latex)
    1.12 +  "{}" ("\<emptyset>")
    1.13  
    1.14  (* insert *)
    1.15  translations 
    1.16    "{x} \<union> A" <= "insert x A"
    1.17    "{x,y}" <= "{x} \<union> {y}"
    1.18    "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    1.19 -  "{x}" <= "{x} \<union> _emptyset"
    1.20 +  "{x}" <= "{x} \<union> \<emptyset>"
    1.21  
    1.22  (* set comprehension *)
    1.23  syntax (latex output)