diff -r d8ca2d0e81e5 -r e322abb912af src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Dec 15 09:44:50 2022 +0100
+++ b/src/HOL/Relation.thy	Thu Dec 15 10:51:46 2022 +0100
@@ -449,13 +449,21 @@
 
 lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV]
 
+lemma antisym_onI:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym_on A r"
+  unfolding antisym_on_def by simp
+
 lemma antisymI [intro?]:
   "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"
-  unfolding antisym_def by iprover
+  by (simp add: antisym_onI)
+
+lemma antisymp_onI:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp_on A R"
+  by (rule antisym_onI[to_pred])
 
 lemma antisympI [intro?]:
-  "(\<And>x y. r x y \<Longrightarrow> r y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp r"
-  by (fact antisymI [to_pred])
+  "(\<And>x y. R x y \<Longrightarrow> R y x \<Longrightarrow> x = y) \<Longrightarrow> antisymp R"
+  by (rule antisymI[to_pred])
     
 lemma antisymD [dest?]:
   "antisym r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> (b, a) \<in> r \<Longrightarrow> a = b"