# HG changeset patch
# User nipkow
# Date 1735400337 -3600
# Node ID 4219bb3951deceb9a1ccf2dde151c68df83ab4b7
# Parent  ece4941f0f1786e9c0c268ca3f62e46ff797fd82# Parent  f1890ac35726e1a6378bfd1065bb148a618e7d16
merged

diff -r ece4941f0f17 -r 4219bb3951de src/HOL/IMP/Live_True.thy
--- a/src/HOL/IMP/Live_True.thy	Fri Dec 27 19:57:55 2024 +0100
+++ b/src/HOL/IMP/Live_True.thy	Sat Dec 28 16:38:57 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)"