more pretty set comprehension sugar
authornipkow
Sun, 13 Feb 2011 08:47:36 +0100
changeset 41757 7bbd11360bd3
parent 41756 e4dbd12a3d83
child 41758 a231e6110f9b
more pretty set comprehension sugar
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 *)