# HG changeset patch
# User nipkow
# Date 1733921075 -3600
# Node ID ecd6752956206e577575a57f23f42d049ff35c84
# Parent  8a360893360759efbe462e422c86226d7b29746b# Parent  1c2a68bb0ff16fee5d68114ab2ce8954208baead
merged

diff -r 8a3608933607 -r ecd675295620 src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Wed Dec 11 12:04:27 2024 +0100
+++ b/src/HOL/IMP/Live_True.thy	Wed Dec 11 13:44:35 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)"