src/HOL/Set.thy
changeset 37387 3581483cca6c
parent 36009 9cdbc5ffc15c
child 37677 c5a8b612e571
     1.1 --- a/src/HOL/Set.thy	Tue Jun 08 07:45:39 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Jun 08 16:37:19 2010 +0200
     1.3 @@ -151,17 +151,11 @@
     1.4    supset_eq  ("op \<supseteq>") and
     1.5    supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
     1.6  
     1.7 -global
     1.8 -
     1.9 -consts
    1.10 -  Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    1.11 -  Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    1.12 +definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.13 +  "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"
    1.14  
    1.15 -local
    1.16 -
    1.17 -defs
    1.18 -  Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
    1.19 -  Bex_def:      "Bex A P        == EX x. x:A & P(x)"
    1.20 +definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.21 +  "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   -- "bounded existential quantifiers"
    1.22  
    1.23  syntax
    1.24    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)