From 56bd4157f59bc6620fef5cd55491c465861dbfc3 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Thu, 31 Aug 2023 14:40:38 +1000
Subject: [PATCH] squash lib/monads: add symmetric bipred_disj_op_eq

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Monads/Fun_Pred_Syntax.thy | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy
index 330034b136..691b929717 100644
--- a/lib/Monads/Fun_Pred_Syntax.thy
+++ b/lib/Monads/Fun_Pred_Syntax.thy
@@ -177,9 +177,8 @@ subsection "Simplification Rules for Lifted And/Or"
 
 lemma bipred_disj_op_eq[simp]:
   "reflp R \<Longrightarrow> ((=) or R) = R"
-  apply (rule ext, rule ext)
-  apply (auto simp: reflp_def)
-  done
+  "reflp R \<Longrightarrow> (R or (=)) = R"
+  by (auto simp: reflp_def)
 
 lemma bipred_le_true[simp]: "R \<le> \<top>\<top>"
   by clarsimp