tuned
authornipkow
Sun Apr 10 11:42:07 2005 +0200 (2005-04-10)
changeset 156901da2cfd1ca45
parent 15689 621bd0d8048f
child 15691 900cf45ff0a6
tuned
src/HOL/Library/LaTeXsugar.thy
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sun Apr 10 11:41:29 2005 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Sun Apr 10 11:42:07 2005 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4  (* insert *)
     1.5  translations 
     1.6    "{x} \<union> A" <= "insert x A"
     1.7 +  "{x,y}" <= "{x} \<union> {y}"
     1.8    "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"
     1.9    "{x}" <= "{x} \<union> _emptyset"
    1.10  
    1.11 @@ -39,6 +40,7 @@
    1.12    "_Collect" :: "pttrn => bool => 'a set"              ("(1{_ | _})")
    1.13  translations
    1.14    "_Collect p P"      <= "{p. P}"
    1.15 +  "_Collect p P"      <= "{p|xs. P}"
    1.16  
    1.17  (* LISTS *)
    1.18