diff -r 63fed88fe8e6 -r e5eb247ad13c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Mar 04 12:28:48 1996 +0100
+++ b/src/HOL/Set.thy	Mon Mar 04 14:37:33 1996 +0100
@@ -37,6 +37,8 @@
 
 syntax
 
+  UNIV         :: 'a set
+
   "~:"          :: ['a, 'a set] => bool             (infixl 50)
 
   "@Finset"     :: args => 'a set                   ("{(_)}")
@@ -57,6 +59,7 @@
   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" 10)
 
 translations
+  "UNIV"        == "Compl {}"
   "x ~: y"      == "~ (x : y)"
   "{x, xs}"     == "insert x {xs}"
   "{x}"         == "insert x {}"