# HG changeset patch # User nipkow # Date 1733921056 -3600 # Node ID 1c2a68bb0ff16fee5d68114ab2ce8954208baead # Parent a180b070d4f8d6077f14a9ef9b00981843da7b74 tuned slow proof diff -r a180b070d4f8 -r 1c2a68bb0ff1 src/HOL/IMP/Live_True.thy --- a/src/HOL/IMP/Live_True.thy Tue Dec 10 19:47:47 2024 +0100 +++ b/src/HOL/IMP/Live_True.thy Wed Dec 11 13:44:16 2024 +0100 @@ -33,7 +33,7 @@ lemma mono_union_L: "mono (\Y. X \ 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 \ X \ L c (L (WHILE b DO c) X)"