# HG changeset patch
# User haftmann
# Date 1184874464 -7200
# Node ID ad26287a9ccb25d2b37172a24c67b65ca27fb884
# Parent  ebec38420a85e190f4f9fb7bc86772317934f9cc
code lemma for contents

diff -r ebec38420a85 -r ad26287a9ccb src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Jul 19 21:47:43 2007 +0200
+++ b/src/HOL/Set.thy	Thu Jul 19 21:47:44 2007 +0200
@@ -2105,9 +2105,10 @@
 
 constdefs
   contents :: "'a set => 'a"
-   "contents X == THE x. X = {x}"
-
-lemma contents_eq [simp]: "contents {x} = x"
+  "contents X == THE x. X = {x}"
+lemmas [code func del] = contents_def
+
+lemma contents_eq [simp, code func]: "contents {x} = x"
 by (simp add: contents_def)