src/HOL/Set.thy
changeset 2006 72754e060aa2
parent 1962 e60a230da179
child 2261 d926157c0a6a
     1.1 --- a/src/HOL/Set.thy	Mon Sep 23 17:46:12 1996 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Sep 23 17:47:49 1996 +0200
     1.3 @@ -32,14 +32,16 @@
     1.4    inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
     1.5    inj_onto      :: ['a => 'b, 'a set] => bool
     1.6    "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
     1.7 -  ":"           :: ['a, 'a set] => bool             (infixl 50) (*membership*)
     1.8 +     (*membership*)
     1.9 +  "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50,51] 50)
    1.10  
    1.11  
    1.12  syntax
    1.13  
    1.14    UNIV         :: 'a set
    1.15  
    1.16 -  "~:"          :: ['a, 'a set] => bool             (infixl 50)
    1.17 +     (*infix synatx for non-membership*)
    1.18 +  "op ~:"        :: ['a, 'a set] => bool             ("(_/ ~: _)" [50,51] 50)
    1.19  
    1.20    "@Finset"     :: args => 'a set                   ("{(_)}")
    1.21