improved subscript syntax;
authorwenzelm
Sat May 01 22:04:14 2004 +0200 (2004-05-01)
changeset 14692b8d6c395c9e2
parent 14691 e1eedc8cad37
child 14693 4deda204e1d8
improved subscript syntax;
src/HOL/Set.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Set.thy	Sat May 01 22:01:57 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Sat May 01 22:04:14 2004 +0200
     1.3 @@ -41,8 +41,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -instance set :: (type) ord ..
     1.8 -instance set :: (type) minus ..
     1.9 +instance set :: (type) "{ord, minus}" ..
    1.10  
    1.11  
    1.12  subsection {* Additional concrete syntax *}
    1.13 @@ -129,10 +128,10 @@
    1.14    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
    1.15  
    1.16  syntax (xsymbols)
    1.17 -  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>\<^bsub>_\<^esub>/ _)" 10)
    1.18 -  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>\<^bsub>_\<^esub>/ _)" 10)
    1.19 -  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.20 -  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.21 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>()\<^bsub>_\<^esub>/ _)" 10)
    1.22 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>()\<^bsub>_\<^esub>/ _)" 10)
    1.23 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.24 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>()\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.25  
    1.26  
    1.27  translations
     2.1 --- a/src/HOL/SetInterval.thy	Sat May 01 22:01:57 2004 +0200
     2.2 +++ b/src/HOL/SetInterval.thy	Sat May 01 22:04:14 2004 +0200
     2.3 @@ -49,10 +49,10 @@
     2.4    "@INTER_less" :: "nat => nat => 'b set => 'b set"       ("(3\<Inter> _<_./ _)" 10)
     2.5  
     2.6  syntax (xsymbols)
     2.7 -  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
     2.8 -  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>\<^bsub>_ < _\<^esub>/ _)" 10)
     2.9 -  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ \<le> _\<^esub>/ _)" 10)
    2.10 -  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>\<^bsub>_ < _\<^esub>/ _)" 10)
    2.11 +  "@UNION_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
    2.12 +  "@UNION_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Union>()\<^bsub>_ < _\<^esub>/ _)" 10)
    2.13 +  "@INTER_le"   :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ \<le> _\<^esub>/ _)" 10)
    2.14 +  "@INTER_less" :: "nat \<Rightarrow> nat => 'b set => 'b set"       ("(3\<Inter>()\<^bsub>_ < _\<^esub>/ _)" 10)
    2.15  
    2.16  translations
    2.17    "UN i<=n. A"  == "UN i:{..n}. A"