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 *}