src/HOL/Set.thy
changeset 3820 46b255e140dc
parent 3370 5c5fdce3a4e4
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/Set.thy	Thu Oct 09 15:01:11 1997 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Oct 09 15:03:06 1997 +0200
     1.3 @@ -18,6 +18,9 @@
     1.4  instance
     1.5    set :: (term) {ord, minus, power}
     1.6  
     1.7 +syntax
     1.8 +  "op :"        :: ['a, 'a set] => bool             ("op :")
     1.9 +
    1.10  consts
    1.11    "{}"          :: 'a set                           ("{}")
    1.12    insert        :: ['a, 'a set] => 'a set
    1.13 @@ -42,14 +45,12 @@
    1.14  
    1.15  syntax
    1.16  
    1.17 -  "op :"        :: ['a, 'a set] => bool               ("op :")
    1.18 -
    1.19    UNIV          :: 'a set
    1.20  
    1.21    (* Infix syntax for non-membership *)
    1.22  
    1.23 +  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    1.24    "op ~:"       :: ['a, 'a set] => bool               ("(_/ ~: _)" [50, 51] 50)
    1.25 -  "op ~:"       :: ['a, 'a set] => bool               ("op ~:")
    1.26  
    1.27    "@Finset"     :: args => 'a set                     ("{(_)}")
    1.28  
    1.29 @@ -83,22 +84,22 @@
    1.30    "EX x:A. P"   => "Bex A (%x. P)"
    1.31  
    1.32  syntax ("" output)
    1.33 +  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
    1.34    "_setle"      :: ['a set, 'a set] => bool           ("(_/ <= _)" [50, 51] 50)
    1.35 -  "_setle"      :: ['a set, 'a set] => bool           ("op <=")
    1.36 +  "_setless"    :: ['a set, 'a set] => bool           ("op <")
    1.37    "_setless"    :: ['a set, 'a set] => bool           ("(_/ < _)" [50, 51] 50)
    1.38 -  "_setless"    :: ['a set, 'a set] => bool           ("op <")
    1.39  
    1.40  syntax (symbols)
    1.41 +  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
    1.42    "_setle"      :: ['a set, 'a set] => bool           ("(_/ \\<subseteq> _)" [50, 51] 50)
    1.43 -  "_setle"      :: ['a set, 'a set] => bool           ("op \\<subseteq>")
    1.44 +  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
    1.45    "_setless"    :: ['a set, 'a set] => bool           ("(_/ \\<subset> _)" [50, 51] 50)
    1.46 -  "_setless"    :: ['a set, 'a set] => bool           ("op \\<subset>")
    1.47    "op Int"      :: ['a set, 'a set] => 'a set         (infixl "\\<inter>" 70)
    1.48    "op Un"       :: ['a set, 'a set] => 'a set         (infixl "\\<union>" 65)
    1.49 +  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
    1.50    "op :"        :: ['a, 'a set] => bool               ("(_/ \\<in> _)" [50, 51] 50)
    1.51 -  "op :"        :: ['a, 'a set] => bool               ("op \\<in>")
    1.52 +  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
    1.53    "op ~:"       :: ['a, 'a set] => bool               ("(_/ \\<notin> _)" [50, 51] 50)
    1.54 -  "op ~:"       :: ['a, 'a set] => bool               ("op \\<notin>")
    1.55    "UN "         :: [idts, bool] => bool               ("(3\\<Union> _./ _)" 10)
    1.56    "INT "        :: [idts, bool] => bool               ("(3\\<Inter> _./ _)" 10)
    1.57    "@UNION"      :: [pttrn, 'a set, 'b set] => 'b set  ("(3\\<Union> _\\<in>_./ _)" 10)