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/Library/Indicator_Function.thy
changeset 75087 f3fcc7c5a0db
parent 73928 3b76524f5a85 
--- a/src/HOL/Library/Indicator_Function.thy	Thu Feb 17 19:42:15 2022 +0000
+++ b/src/HOL/Library/Indicator_Function.thy	Thu Feb 17 19:42:16 2022 +0000
@@ -208,6 +208,6 @@
 lemma indicator_UN_disjoint:
   "finite A \<Longrightarrow> disjoint_family_on f A \<Longrightarrow> indicator (\<Union>(f ` A)) x = (\<Sum>y\<in>A. indicator (f y) x)"
   by (induct A rule: finite_induct)
-    (auto simp: disjoint_family_on_def indicator_def split: if_splits)
+    (auto simp: disjoint_family_on_def indicator_def split: if_splits split_of_bool_asm)
 
 end
isabelle