src/HOL/Set.thy
changeset 1531 e5eb247ad13c
parent 1370 7361ac9b024d
child 1672 2c109cd2fdd0
     1.1 --- a/src/HOL/Set.thy	Mon Mar 04 12:28:48 1996 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Mar 04 14:37:33 1996 +0100
     1.3 @@ -37,6 +37,8 @@
     1.4  
     1.5  syntax
     1.6  
     1.7 +  UNIV         :: 'a set
     1.8 +
     1.9    "~:"          :: ['a, 'a set] => bool             (infixl 50)
    1.10  
    1.11    "@Finset"     :: args => 'a set                   ("{(_)}")
    1.12 @@ -57,6 +59,7 @@
    1.13    "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
    1.14  
    1.15  translations
    1.16 +  "UNIV"        == "Compl {}"
    1.17    "x ~: y"      == "~ (x : y)"
    1.18    "{x, xs}"     == "insert x {xs}"
    1.19    "{x}"         == "insert x {}"