src/HOL/Relation.thy
changeset 60057 86fa63ce8156
parent 59518 28cfc60dea7a
child 60758 d8d85a8172b5
--- a/src/HOL/Relation.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Relation.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -216,6 +216,8 @@
   "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
   by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
 
+lemma reflp_equality [simp]: "reflp op ="
+by(simp add: reflp_def)
 
 subsubsection {* Irreflexivity *}
 
@@ -357,6 +359,8 @@
 lemma antisym_empty [simp]: "antisym {}"
   by (unfold antisym_def) blast
 
+lemma antisymP_equality [simp]: "antisymP op ="
+by(auto intro: antisymI)
 
 subsubsection {* Transitivity *}