# HG changeset patch
# User huffman
# Date 1333632206 -7200
# Node ID 8e6a45f1bf8fed26ce6849c7781656d5aa766c35
# Parent  9475d524bafb039006242e5485c28c2368b315b6
define reflp directly, in the manner of symp and transp

diff -r 9475d524bafb -r 8e6a45f1bf8f src/HOL/Relation.thy
--- 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"