src/HOL/Set.thy
changeset 14565 c6dc17aab88a
parent 14551 2cb6ff394bfb
child 14692 b8d6c395c9e2
     1.1 --- a/src/HOL/Set.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -108,6 +108,20 @@
     1.4    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
     1.5    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
     1.6  
     1.7 +syntax (HTML output)
     1.8 +  "_setle"      :: "'a set => 'a set => bool"             ("op \<subseteq>")
     1.9 +  "_setle"      :: "'a set => 'a set => bool"             ("(_/ \<subseteq> _)" [50, 51] 50)
    1.10 +  "_setless"    :: "'a set => 'a set => bool"             ("op \<subset>")
    1.11 +  "_setless"    :: "'a set => 'a set => bool"             ("(_/ \<subset> _)" [50, 51] 50)
    1.12 +  "op Int"      :: "'a set => 'a set => 'a set"           (infixl "\<inter>" 70)
    1.13 +  "op Un"       :: "'a set => 'a set => 'a set"           (infixl "\<union>" 65)
    1.14 +  "op :"        :: "'a => 'a set => bool"                 ("op \<in>")
    1.15 +  "op :"        :: "'a => 'a set => bool"                 ("(_/ \<in> _)" [50, 51] 50)
    1.16 +  "op ~:"       :: "'a => 'a set => bool"                 ("op \<notin>")
    1.17 +  "op ~:"       :: "'a => 'a set => bool"                 ("(_/ \<notin> _)" [50, 51] 50)
    1.18 +  "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
    1.19 +  "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
    1.20 +
    1.21  syntax (input)
    1.22    "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" 10)
    1.23    "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" 10)
    1.24 @@ -120,6 +134,7 @@
    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 +
    1.29  translations
    1.30    "op \<subseteq>" => "op <= :: _ set => _ set => bool"
    1.31    "op \<subset>" => "op <  :: _ set => _ set => bool"