src/HOL/Set.thy
 changeset 31991 37390299214a parent 31945 d5f186aa0bed child 32010 cb1a1c94b4cd child 32064 53ca12ff305d
```     1.1 --- a/src/HOL/Set.thy	Fri Jul 10 09:24:50 2009 +0200
1.2 +++ b/src/HOL/Set.thy	Sat Jul 11 21:33:01 2009 +0200
1.3 @@ -10,7 +10,6 @@
1.4
1.5  text {* A set in HOL is simply a predicate. *}
1.6
1.7 -
1.8  subsection {* Basic syntax *}
1.9
1.10  global
1.11 @@ -363,46 +362,6 @@
1.12    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
1.13    Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
1.14
1.15 -instantiation "fun" :: (type, minus) minus
1.16 -begin
1.17 -
1.18 -definition
1.19 -  fun_diff_def: "A - B = (%x. A x - B x)"
1.20 -
1.21 -instance ..
1.22 -
1.23 -end
1.24 -
1.25 -instantiation bool :: minus
1.26 -begin
1.27 -
1.28 -definition
1.29 -  bool_diff_def: "A - B = (A & ~ B)"
1.30 -
1.31 -instance ..
1.32 -
1.33 -end
1.34 -
1.35 -instantiation "fun" :: (type, uminus) uminus
1.36 -begin
1.37 -
1.38 -definition
1.39 -  fun_Compl_def: "- A = (%x. - A x)"
1.40 -
1.41 -instance ..
1.42 -
1.43 -end
1.44 -
1.45 -instantiation bool :: uminus
1.46 -begin
1.47 -
1.48 -definition
1.49 -  bool_Compl_def: "- A = (~ A)"
1.50 -
1.51 -instance ..
1.52 -
1.53 -end
1.54 -
1.55  definition Pow :: "'a set => 'a set set" where
1.56    Pow_def: "Pow A = {B. B \<le> A}"
1.57
```