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/ZF/UNITY/MultisetSum.thy
changeset 32960 69916a850301
parent 24893 b8ef7afe3a6b
child 37936 1e4c5015a72e 
--- a/src/ZF/UNITY/MultisetSum.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/ZF/UNITY/MultisetSum.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      ZF/UNITY/MultusetSum.thy
-    ID:         $Id$
     Author:     Sidi O Ehmety
 *)
 
@@ -122,7 +121,7 @@
      "[| I \<in> Fin(K); \<forall>i \<in> K. C(i) \<in> Fin(A) |] ==>  
       (\<forall>x \<in> A. multiset(f(x)) & mset_of(f(x))\<subseteq>B) -->   
       (\<forall>i \<in> I. \<forall>j \<in> I. i\<noteq>j --> C(i) Int C(j) = 0) -->  
-	msetsum(f, \<Union>i \<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"
+        msetsum(f, \<Union>i \<in> I. C(i), B) = msetsum (%i. msetsum(f, C(i),B), I, B)"
 apply (erule Fin_induct, auto)
 apply (subgoal_tac "\<forall>i \<in> y. x \<noteq> i")
  prefer 2 apply blast
isabelle