# HG changeset patch
# User nipkow
# Date 1113126127 -7200
# Node ID 1da2cfd1ca452ae10d347a09d1c33d07f1a2ff2a
# Parent  621bd0d8048fe3b05be270b6c58efaaf948d7338
tuned

diff -r 621bd0d8048f -r 1da2cfd1ca45 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 *)