src/HOL/Library/LaTeXsugar.thy

--- a/src/HOL/Library/LaTeXsugar.thy	Sun Apr 10 11:41:29 2005 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy	Sun Apr 10 11:42:07 2005 +0200
@@ -31,6 +31,7 @@
 (* insert *)
 translations 
   "{x} \<union> A" <= "insert x A"
+  "{x,y}" <= "{x} \<union> {y}"
   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
   "{x}" <= "{x} \<union> _emptyset"
 
@@ -39,6 +40,7 @@
   "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
 translations
   "_Collect p P"      <= "{p. P}"
+  "_Collect p P"      <= "{p|xs. P}"
 
 (* LISTS *)