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/Transitive_Closure.thy
changeset 69276 3d954183b707
parent 68618 3db8520941a4
child 69593 3dda49e08b9d 
--- a/src/HOL/Transitive_Closure.thy	Sat Nov 10 07:57:19 2018 +0000
+++ b/src/HOL/Transitive_Closure.thy	Sat Nov 10 07:57:20 2018 +0000
@@ -1064,7 +1064,7 @@
 lemma relpow_finite_bounded:
   fixes R :: "('a \<times> 'a) set"
   assumes "finite R"
-  shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)"
+  shows "R^^k \<subseteq> (\<Union>n\<in>{n. n \<le> card R}. R^^n)"
   apply (cases k, force)
   apply (use relpow_finite_bounded1[OF assms, of k] in auto)
   done
isabelle