# HG changeset patch
# User bulwahn
# Date 1291725208 -3600
# Node ID dcec9bc71ee9f12dd0b36b0a09c350551ed4fe66
# Parent  d6f45159ae84241eef6cf3eb6f953178f90b3cab
adding a definition for refl_on which is friendly for quickcheck and nitpick

diff -r d6f45159ae84 -r dcec9bc71ee9 src/HOL/Relation.thy
--- 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 *}