src/HOL/Set.thy
changeset 37767 a2b7a20d6ea3
parent 37677 c5a8b612e571
child 38648 52ea97d95e4b
     1.1 --- a/src/HOL/Set.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -1574,7 +1574,7 @@
     1.4  subsubsection {* Inverse image of a function *}
     1.5  
     1.6  definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
     1.7 -  [code del]: "f -` B == {x. f x : B}"
     1.8 +  "f -` B == {x. f x : B}"
     1.9  
    1.10  lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
    1.11    by (unfold vimage_def) blast
    1.12 @@ -1657,7 +1657,7 @@
    1.13  subsubsection {* Getting the Contents of a Singleton Set *}
    1.14  
    1.15  definition contents :: "'a set \<Rightarrow> 'a" where
    1.16 -  [code del]: "contents X = (THE x. X = {x})"
    1.17 +  "contents X = (THE x. X = {x})"
    1.18  
    1.19  lemma contents_eq [simp]: "contents {x} = x"
    1.20    by (simp add: contents_def)