adding a definition for refl_on which is friendly for quickcheck and nitpick

--- a/src/HOL/Relation.thy	Tue Dec 07 12:10:13 2010 +0100
+++ b/src/HOL/Relation.thy	Tue Dec 07 13:33:28 2010 +0100
@@ -227,6 +227,9 @@
 lemma refl_on_Id_on: "refl_on A (Id_on A)"
 by (rule refl_onI [OF Id_on_subset_Times Id_onI])
 
+lemma refl_on_def'[nitpick_def, code]:
+  "refl_on A r = ((\<forall>(x, y) \<in> r. x : A \<and> y : A) \<and> (\<forall>x \<in> A. (x, x) : r))"
+by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
 
 subsection {* Antisymmetry *}