Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned slow proof
authornipkow
Wed, 11 Dec 2024 13:44:16 +0100
changeset 81676 1c2a68bb0ff1
parent 81571 a180b070d4f8
child 81677 ecd675295620
tuned slow proof
src/HOL/IMP/Live_True.thy file | annotate | diff | comparison | revisions 
--- 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 (\<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)"
isabelle