src/HOL/Set.thy
 changeset 31643 b040f1679f77 parent 31461 d54b743b52a3 child 31945 d5f186aa0bed
```     1.1 --- a/src/HOL/Set.thy	Mon Jun 15 16:13:04 2009 +0200
1.2 +++ b/src/HOL/Set.thy	Mon Jun 15 16:13:19 2009 +0200
1.3 @@ -23,8 +23,6 @@
1.4    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
1.5    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
1.6    Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
1.7 -  Pow           :: "'a set => 'a set set"                -- "powerset"
1.8 -  image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
1.9
1.10  local
1.11
1.12 @@ -215,9 +213,6 @@
1.13    supset_eq  ("op \<supseteq>") and
1.14    supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
1.15
1.16 -abbreviation
1.17 -  range :: "('a => 'b) => 'b set" where -- "of function"
1.18 -  "range f == f ` UNIV"
1.19
1.20
1.21  subsubsection "Bounded quantifiers"
1.22 @@ -408,9 +403,15 @@
1.23
1.24  end
1.25
1.26 -defs
1.27 -  Pow_def:      "Pow A          == {B. B <= A}"
1.28 -  image_def:    "f`A            == {y. EX x:A. y = f(x)}"
1.29 +definition Pow :: "'a set => 'a set set" where
1.30 +  Pow_def: "Pow A = {B. B \<le> A}"
1.31 +
1.32 +definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
1.33 +  image_def: "f ` A = {y. EX x:A. y = f(x)}"
1.34 +
1.35 +abbreviation
1.36 +  range :: "('a => 'b) => 'b set" where -- "of function"
1.37 +  "range f == f ` UNIV"
1.38
1.39
1.40  subsection {* Lemmas and proof tool setup *}
```