# HG changeset patch # User haftmann # Date 1268319154 -3600 # Node ID 3cd1e4b651115ab5e0b708b01a2ae18c4b2648f5 # Parent c36ade6f4c33e515a9cd8bb1ebad3a7c2271b0f4 replaced card_def by card_eq_setsum diff -r c36ade6f4c33 -r 3cd1e4b65111 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Mar 11 15:52:33 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Mar 11 15:52:34 2010 +0100 @@ -94,8 +94,8 @@ using lem1[unfolded lem3 lem2 lem5] by auto have even_minus_odd:"\x y. even x \ odd (y::int) \ odd (x - y)" using assms by auto have odd_minus_even:"\x y. odd x \ even (y::int) \ odd (x - y)" using assms by auto - show ?thesis unfolding even_nat_def unfolding card_def and lem4[THEN sym] and *[unfolded card_def] - unfolding card_def[THEN sym] apply(rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even) + show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum] + unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even) apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed subsection {* The odd/even result for faces of complete vertices, generalized. *}