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