Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Free_Abelian_Groups.thy
changeset 73932 fd21b4a93043
parent 73348 65c45cba3f54 
--- a/src/HOL/Algebra/Free_Abelian_Groups.thy	Fri Jun 18 15:03:12 2021 +0200
+++ b/src/HOL/Algebra/Free_Abelian_Groups.thy	Thu Jul 08 08:42:36 2021 +0200
@@ -242,7 +242,7 @@
 lemma sum_closed_free_Abelian_group:
     "(\<And>i. i \<in> I \<Longrightarrow> x i \<in> carrier (free_Abelian_group S)) \<Longrightarrow> sum x I \<in> carrier (free_Abelian_group S)"
   apply (induction I rule: infinite_finite_induct, auto)
-  by (metis (no_types, hide_lams) UnE subsetCE keys_add)
+  by (metis (no_types, opaque_lifting) UnE subsetCE keys_add)
 
 
 lemma (in comm_group) free_Abelian_group_universal:
isabelle