Modified UN and INT xsymbol syntax: made index subscript
authornipkow
Wed Feb 11 01:26:15 2004 +0100 (2004-02-11)
changeset 143811189a8212a12
parent 14380 04b603a6f17d
child 14382 9fb68cd74719
Modified UN and INT xsymbol syntax: made index subscript
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Wed Feb 11 00:37:18 2004 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Feb 11 01:26:15 2004 +0100
     1.3 @@ -103,14 +103,22 @@
     1.4    "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
     1.5    "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
     1.6    "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
     1.7 +  Union         :: "'a set set => 'a set"                 ("\<Union>_" [90] 90)
     1.8 +  Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
     1.9 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
    1.10 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
    1.11 +
    1.12 +syntax (input)
    1.13    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
    1.14    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
    1.15    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" 10)
    1.16    "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" 10)
    1.17 -  Union         :: "'a set set => 'a set"                 ("\<Union>_" [90] 90)
    1.18 -  Inter         :: "'a set set => 'a set"                 ("\<Inter>_" [90] 90)
    1.19 -  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
    1.20 -  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
    1.21 +
    1.22 +syntax (xsymbols)
    1.23 +  "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>\<^bsub>_\<^esub>/ _)" 10)
    1.24 +  "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>\<^bsub>_\<^esub>/ _)" 10)
    1.25 +  "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.26 +  "@INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>\<^bsub>_\<in>_\<^esub>/ _)" 10)
    1.27  
    1.28  translations
    1.29    "op \<subseteq>" => "op <= :: _ set => _ set => bool"