src/HOL/Set.thy
changeset 25762 c03e9d04b3e4
parent 25510 38c15efe603b
child 25965 05df64f786a4
     1.1 --- a/src/HOL/Set.thy	Wed Jan 02 12:22:38 2008 +0100
     1.2 +++ b/src/HOL/Set.thy	Wed Jan 02 15:14:02 2008 +0100
     1.3 @@ -352,10 +352,17 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  Compl_def [code func del]:    "- A   = {x. ~x:A}"
     1.8 +  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
     1.9 +
    1.10 +instance ..
    1.11 +
    1.12 +end
    1.13 +
    1.14 +instantiation set :: (type) uminus
    1.15 +begin
    1.16  
    1.17  definition
    1.18 -  set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}"
    1.19 +  Compl_def [code func del]:    "- A   = {x. ~x:A}"
    1.20  
    1.21  instance ..
    1.22