src/HOL/Set.thy
changeset 25510 38c15efe603b
parent 25502 9200b36280c0
child 25762 c03e9d04b3e4
     1.1 --- a/src/HOL/Set.thy	Fri Nov 30 16:23:52 2007 +0100
     1.2 +++ b/src/HOL/Set.thy	Fri Nov 30 20:13:03 2007 +0100
     1.3 @@ -143,10 +143,18 @@
     1.4    union/intersection symbol because this leads to problems with nested
     1.5    subscripts in Proof General. *}
     1.6  
     1.7 -instance set :: (type) ord
     1.8 -  subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
     1.9 -  psubset_def: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
    1.10 -lemmas [code func del] = subset_def psubset_def
    1.11 +instantiation set :: (type) ord
    1.12 +begin
    1.13 +
    1.14 +definition
    1.15 +  subset_def [code func del]: "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
    1.16 +
    1.17 +definition
    1.18 +  psubset_def [code func del]: "(A\<Colon>'a set) < B \<equiv> A \<le> B \<and> A \<noteq> B"
    1.19 +
    1.20 +instance ..
    1.21 +
    1.22 +end
    1.23  
    1.24  abbreviation
    1.25    subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.26 @@ -340,11 +348,18 @@
    1.27    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
    1.28    Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
    1.29  
    1.30 -instance set :: (type) minus
    1.31 -  Compl_def:    "- A            == {x. ~x:A}"
    1.32 -  set_diff_def: "A - B          == {x. x:A & ~x:B}" ..
    1.33 -
    1.34 -lemmas [code func del] = Compl_def set_diff_def
    1.35 +instantiation set :: (type) minus
    1.36 +begin
    1.37 +
    1.38 +definition
    1.39 +  Compl_def [code func del]:    "- A   = {x. ~x:A}"
    1.40 +
    1.41 +definition
    1.42 +  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
    1.43 +
    1.44 +instance ..
    1.45 +
    1.46 +end
    1.47  
    1.48  defs
    1.49    Un_def:       "A Un B         == {x. x:A | x:B}"