src/HOL/Set.thy
 changeset 34999 5312d2ffee3b parent 34974 18b41bba42b5 child 35115 446c5063e4fd
```     1.1 --- a/src/HOL/Set.thy	Thu Feb 04 13:36:52 2010 +0100
1.2 +++ b/src/HOL/Set.thy	Thu Feb 04 14:45:08 2010 +0100
1.3 @@ -161,14 +161,12 @@
1.4  consts
1.5    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
1.6    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
1.7 -  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
1.8
1.9  local
1.10
1.11  defs
1.12    Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
1.13    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
1.14 -  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
1.15
1.16  syntax
1.17    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
1.18 @@ -195,7 +193,7 @@
1.19  translations
1.20    "ALL x:A. P"  == "Ball A (%x. P)"
1.21    "EX x:A. P"   == "Bex A (%x. P)"
1.22 -  "EX! x:A. P"  == "Bex1 A (%x. P)"
1.23 +  "EX! x:A. P"  => "EX! x. x:A & P"
1.24    "LEAST x:A. P" => "LEAST x. x:A & P"
1.25
1.26  syntax (output)
```