src/HOL/Set.thy
 changeset 13764 3e180bf68496 parent 13763 f94b569cd610 child 13818 274fda8cca4b
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.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.30          fun tr' (_ \$ abs) =
1.31            let val _ \$ idts \$ (_ \$ (_ \$ _ \$ e) \$ Q) = ex_tr' [abs]