define reflp directly, in the manner of symp and transp

--- a/src/HOL/Relation.thy	Thu Apr 05 14:14:16 2012 +0200
+++ b/src/HOL/Relation.thy	Thu Apr 05 15:23:26 2012 +0200
@@ -146,7 +146,7 @@
 
 definition reflp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
 where
-  "reflp r \<longleftrightarrow> refl {(x, y). r x y}"
+  "reflp r \<longleftrightarrow> (\<forall>x. r x x)"
 
 lemma reflp_refl_eq [pred_set_conv]:
   "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"