# HG changeset patch
# User nipkow
# Date 1345186568 -7200
# Node ID efb8641b4944e85b977a0aeabc6472824f57db8e
# Parent  722de4ae08cb8b19c31277291075faeefd69df77
fixed lemmas

diff -r 722de4ae08cb -r efb8641b4944 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Aug 16 15:08:42 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Fri Aug 17 08:56:08 2012 +0200
@@ -65,13 +65,18 @@
     by (simp add: union_disjoint[OF f d, unfolded eq[symmetric]] F_neutral'[OF assms(3)])
 qed
 
-lemmas F_mono_neutral_cong_right = F_mono_neutral_cong_left[symmetric]
+lemma F_mono_neutral_cong_right:
+  "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk>
+   \<Longrightarrow> F g T = F h S"
+by(auto intro!: F_mono_neutral_cong_left[symmetric])
 
 lemma F_mono_neutral_left:
   "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T"
 by(blast intro: F_mono_neutral_cong_left)
 
-lemmas F_mono_neutral_right = F_mono_neutral_left[symmetric]
+lemma F_mono_neutral_right:
+  "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
+by(blast intro!: F_mono_neutral_left[symmetric])
 
 lemma F_delta: 
   assumes fS: "finite S"