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)
```