1.1 --- a/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Jul 01 16:54:42 2010 +0200
     1.3 @@ -8,42 +8,36 @@
     1.4  
     1.5  subsection {* Sets as predicates *}
     1.6  
     1.7 -global
     1.8 -
     1.9 -types 'a set = "'a => bool"
    1.10 +types 'a set = "'a \<Rightarrow> bool"
    1.11  
    1.12 -consts
    1.13 -  Collect       :: "('a => bool) => 'a set"              -- "comprehension"
    1.14 -  "op :"        :: "'a => 'a set => bool"                -- "membership"
    1.15 +definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
    1.16 +  "Collect P = P"
    1.17  
    1.18 -local
    1.19 +definition member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" where -- "membership"
    1.20 +  mem_def: "member x A = A x"
    1.21  
    1.22  notation
    1.23 -  "op :"  ("op :") and
    1.24 -  "op :"  ("(_/ : _)" [50, 51] 50)
    1.25 +  member  ("op :") and
    1.26 +  member  ("(_/ : _)" [50, 51] 50)
    1.27  
    1.28 -defs
    1.29 -  mem_def [code]: "x : S == S x"
    1.30 -  Collect_def [code]: "Collect P == P"
    1.31 -
    1.32 -abbreviation
    1.33 -  "not_mem x A == ~ (x : A)" -- "non-membership"
    1.34 +abbreviation not_member where
    1.35 +  "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
    1.36  
    1.37  notation
    1.38 -  not_mem  ("op ~:") and
    1.39 -  not_mem  ("(_/ ~: _)" [50, 51] 50)
    1.40 +  not_member  ("op ~:") and
    1.41 +  not_member  ("(_/ ~: _)" [50, 51] 50)
    1.42  
    1.43  notation (xsymbols)
    1.44 -  "op :"  ("op \<in>") and
    1.45 -  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
    1.46 -  not_mem  ("op \<notin>") and
    1.47 -  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
    1.48 +  member      ("op \<in>") and
    1.49 +  member      ("(_/ \<in> _)" [50, 51] 50) and
    1.50 +  not_member  ("op \<notin>") and
    1.51 +  not_member  ("(_/ \<notin> _)" [50, 51] 50)
    1.52  
    1.53  notation (HTML output)
    1.54 -  "op :"  ("op \<in>") and
    1.55 -  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
    1.56 -  not_mem  ("op \<notin>") and
    1.57 -  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
    1.58 +  member      ("op \<in>") and
    1.59 +  member      ("(_/ \<in> _)" [50, 51] 50) and
    1.60 +  not_member  ("op \<notin>") and
    1.61 +  not_member  ("(_/ \<notin> _)" [50, 51] 50)
    1.62  
    1.63  text {* Set comprehensions *}
    1.64  
    1.65 @@ -312,7 +306,7 @@
    1.66          in
    1.67            case t of
    1.68              Const (@{const_syntax "op &"}, _) $
    1.69 -              (Const (@{const_syntax "op :"}, _) $
    1.70 +              (Const (@{const_syntax Set.member}, _) $
    1.71                  (Const (@{syntax_const "_bound"}, _) $ Free (yN, _)) $ A) $ P =>
    1.72              if xN = yN then Syntax.const @{syntax_const "_Collect"} $ x $ A $ P else M
    1.73            | _ => M
    1.74 @@ -922,7 +916,7 @@
    1.75  lemmas split_ifs = if_bool_eq_conj split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
    1.76  
    1.77  (*Would like to add these, but the existing code only searches for the
    1.78 -  outer-level constant, which in this case is just "op :"; we instead need
    1.79 +  outer-level constant, which in this case is just Set.member; we instead need
    1.80    to use term-nets to associate patterns with rules.  Also, if a rule fails to
    1.81    apply, then the formula should be kept.
    1.82    [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
    1.83 @@ -1691,6 +1685,7 @@
    1.84  lemma vimage_code [code]: "(f -` A) x = A (f x)"
    1.85    by (simp add: vimage_def Collect_def mem_def)
    1.86  
    1.87 +hide_const (open) member
    1.88  
    1.89  text {* Misc theorem and ML bindings *}
    1.90