--- 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 *}