# HG changeset patch
# User desharna
# Date 1670176198 -3600
# Node ID e28aed61a4b1fc836672f1a8832c73e2ac1f4ad6
# Parent  120f79cdb492e89ed26801888b66c96a91062547# Parent  a7d9e34c85e6bdc9addeacf734c1b2f6e811056c
merged

diff -r 120f79cdb492 -r e28aed61a4b1 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Dec 04 14:24:42 2022 +0100
+++ b/src/HOL/Relation.thy	Sun Dec 04 18:49:58 2022 +0100
@@ -90,10 +90,10 @@
 lemma bot_empty_eq2 [pred_set_conv]: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
+lemma top_empty_eq: "\<top> = (\<lambda>x. x \<in> UNIV)"
   by (auto simp add: fun_eq_iff)
 
-lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
+lemma top_empty_eq2: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
   by (auto simp add: fun_eq_iff)
 
 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"