src/HOL/Set.thy
changeset 14845 345934d5bc1a
parent 14812 4b2c006d0534
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Set.thy	Sat May 29 15:11:06 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Sat May 29 15:11:43 2004 +0200
     1.3 @@ -128,10 +128,10 @@
     1.4    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>()\<^bsub>_\<^esub>/ _)" 10)
     1.8 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>()\<^bsub>_\<^esub>/ _)" 10)
     1.9 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.10 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.11 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" 10)
    1.12 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" 10)
    1.13 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    1.14 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" 10)
    1.15  
    1.16  
    1.17  translations