\<^bsub>/\<^esub> syntax: unbreakable block;
authorwenzelm
Sat May 29 15:11:43 2004 +0200 (2004-05-29)
changeset 14845345934d5bc1a
parent 14844 a15c65e66ee9
child 14846 b1fcade3880b
\<^bsub>/\<^esub> syntax: unbreakable block;
src/HOL/Set.thy
     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