src/HOL/Library/LaTeXsugar.thy
changeset 41757 7bbd11360bd3
parent 35251 e244adbbc28f
child 49628 8262d35eff20
--- 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 *)