src/HOL/SetInterval.thy
changeset 14846 b1fcade3880b
parent 14692 b8d6c395c9e2
child 15041 a6b1f0cef7b3
     1.1 --- a/src/HOL/SetInterval.thy	Sat May 29 15:11:43 2004 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Sat May 29 16:47:06 2004 +0200
     1.3 @@ -49,10 +49,10 @@
     1.4    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
     1.5  
     1.6  syntax (xsymbols)
     1.7 -  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
     1.8 -  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ < _\<^esub>/ _)" 10)
     1.9 -  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
    1.10 -  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ < _\<^esub>/ _)" 10)
    1.11 +  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
    1.12 +  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
    1.13 +  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ \<le> _\<^esub>)/ _)" 10)
    1.14 +  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>(00\<^bsub>_ < _\<^esub>)/ _)" 10)
    1.15  
    1.16  translations
    1.17    "UN i<=n. A"  == "UN i:{..n}. A"