# HG changeset patch
# User desharna
# Date 1669051495 -3600
# Node ID a7d9e34c85e6bdc9addeacf734c1b2f6e811056c
# Parent  41c92fcb8805d6284e514670d8d9bcf1c4a4a41b
removed prod_set_conv attribute from top_empty_eq and top_empty_eq2

diff -r 41c92fcb8805 -r a7d9e34c85e6 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Nov 21 18:23:32 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Nov 21 18:24:55 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)"