src/HOL/Set.thy

--- a/src/HOL/Set.thy	Fri Aug 17 09:20:45 2007 +0200
+++ b/src/HOL/Set.thy	Fri Aug 17 13:58:57 2007 +0200
@@ -147,7 +147,6 @@
 instance set :: (type) ord
   subset_def:  "A \<le> B \<equiv> \<forall>x\<in>A. x \<in> B"
   psubset_def: "A < B \<equiv> A \<le> B \<and> A \<noteq> B" ..
-
 lemmas [code func del] = subset_def psubset_def
 
 abbreviation