# HG changeset patch
# User nipkow
# Date 1297583256 -3600
# Node ID 7bbd11360bd340cea625eb4cedf4ca656ec1e949
# Parent  e4dbd12a3d8373fc18923802a2135cb57c04da31
more pretty set comprehension sugar

diff -r e4dbd12a3d83 -r 7bbd11360bd3 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Fri Feb 11 15:31:19 2011 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Sun Feb 13 08:47:36 2011 +0100
@@ -42,9 +42,11 @@
 (* set comprehension *)
 syntax (latex output)
   "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
+  "_CollectIn" :: "pttrn => 'a set => bool => 'a set"   ("(1{_ \<in> _ | _})")
 translations
   "_Collect p P"      <= "{p. P}"
   "_Collect p P"      <= "{p|xs. P}"
+  "_CollectIn p A P"  <= "{p : A. P}"
 
 (* LISTS *)