--- a/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 22 12:55:36 2004 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Thu Jul 22 17:37:31 2004 +0200
@@ -71,13 +71,13 @@
declare setsum_cong [cong]
lemma bag_of_sublist_lemma:
- "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =
- (\<Sum>i: A Int lessThan k. {#f i#})"
+ "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =
+ (\<Sum>i\<in> A Int lessThan k. {#f i#})"
by (rule setsum_cong, auto)
lemma bag_of_sublist:
"bag_of (sublist l A) =
- (\<Sum>i: A Int lessThan (length l). {# l!i #})"
+ (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
apply (rule_tac xs = l in rev_induct, simp)
apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append
bag_of_sublist_lemma add_ac)
@@ -101,7 +101,7 @@
lemma bag_of_sublist_UN_disjoint [rule_format]:
"[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]
==> bag_of (sublist l (UNION I A)) =
- (\<Sum>i:I. bag_of (sublist l (A i)))"
+ (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
apply (simp del: UN_simps
add: UN_simps [symmetric] add: bag_of_sublist)
apply (subst setsum_UN_disjoint, auto)