src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
changeset 44821 a92f65e174cf
parent 44457 d366fa5551ef
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -93,7 +93,7 @@
     1.4    have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
     1.5    have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
     1.6    show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]
     1.7 -    unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even)
     1.8 +    unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even)
     1.9      apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed
    1.10  
    1.11  subsection {* The odd/even result for faces of complete vertices, generalized. *}