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)