# HG changeset patch
# User nipkow
# Date 1734515459 -3600
# Node ID f1890ac35726e1a6378bfd1065bb148a618e7d16
# Parent  6528e378be872fed0b45cbf86d8cc1c62b6f23cb# Parent  ecd6752956206e577575a57f23f42d049ff35c84
merged

diff -r 6528e378be87 -r f1890ac35726 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Wed Dec 18 10:43:44 2024 +0100
+++ b/src/HOL/IMP/Live_True.thy	Wed Dec 18 10:50:59 2024 +0100
@@ -33,7 +33,7 @@
 
 lemma mono_union_L:
   "mono (\<lambda>Y. X \<union> L c Y)"
-by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono)
+using L_mono unfolding mono_def by (metis (no_types) order_eq_iff set_eq_subset sup_mono)
 
 lemma L_While_unfold:
   "L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)"