1.1 --- a/src/HOL/Set.thy	Sun Dec 22 10:43:43 2002 +0100
     1.2 +++ b/src/HOL/Set.thy	Sun Dec 22 15:02:40 2002 +0100
     1.3 @@ -74,15 +74,15 @@
     1.4    "x ~: y"      == "~ (x : y)"
     1.5    "{x, xs}"     == "insert x {xs}"
     1.6    "{x}"         == "insert x {}"
     1.7 -  "{x. P}"      => "Collect (%x. P)"
     1.8 +  "{x. P}"      == "Collect (%x. P)"
     1.9    "UN x y. B"   == "UN x. UN y. B"
    1.10    "UN x. B"     == "UNION UNIV (%x. B)"
    1.11    "INT x y. B"  == "INT x. INT y. B"
    1.12    "INT x. B"    == "INTER UNIV (%x. B)"
    1.13 -  "UN x:A. B"   => "UNION A (%x. B)"
    1.14 -  "INT x:A. B"  => "INTER A (%x. B)"
    1.15 -  "ALL x:A. P"  => "Ball A (%x. P)"
    1.16 -  "EX x:A. P"   => "Bex A (%x. P)"
    1.17 +  "UN x:A. B"   == "UNION A (%x. B)"
    1.18 +  "INT x:A. B"  == "INTER A (%x. B)"
    1.19 +  "ALL x:A. P"  == "Ball A (%x. P)"
    1.20 +  "EX x:A. P"   == "Bex A (%x. P)"
    1.21  
    1.22  syntax (output)
    1.23    "_setle"      :: "'a set => 'a set => bool"             ("op <=")
    1.24 @@ -172,6 +172,7 @@
    1.25          | check (Const ("op &", _) $ (Const ("op =", _) $ Bound m $ e) $ P, n) =
    1.26              n > 0 andalso m = n andalso not (loose_bvar1 (P, n)) andalso
    1.27              ((0 upto (n - 1)) subset add_loose_bnos (e, 0, []))
    1.28 +        | check _ = false
    1.29  
    1.30          fun tr' (_ $ abs) =
    1.31            let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr' [abs]