src/HOL/Library/LaTeXsugar.thy
changeset 31462 4fcbf17b5a98
parent 30663 0b6aff7451b2
child 35251 e244adbbc28f
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 08:06:03 2009 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jun 05 08:28:24 2009 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5  (* insert *)
     1.6  translations 
     1.7 -  "{x} \<union> A" <= "insert x A"
     1.8 +  "{x} \<union> A" <= "CONST insert x A"
     1.9    "{x,y}" <= "{x} \<union> {y}"
    1.10    "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
    1.11    "{x}" <= "{x} \<union> \<emptyset>"