| changeset 25762 | c03e9d04b3e4 |
| parent 25510 | 38c15efe603b |
| child 25965 | 05df64f786a4 |
--- a/src/HOL/Set.thy Wed Jan 02 12:22:38 2008 +0100 +++ b/src/HOL/Set.thy Wed Jan 02 15:14:02 2008 +0100 @@ -352,10 +352,17 @@ begin definition - Compl_def [code func del]: "- A = {x. ~x:A}" + set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}" + +instance .. + +end + +instantiation set :: (type) uminus +begin definition - set_diff_def [code func del]: "A - B = {x. x:A & ~x:B}" + Compl_def [code func del]: "- A = {x. ~x:A}" instance ..