--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Jun 10 19:10:20 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Jun 10 20:15:58 2015 +0200
@@ -189,11 +189,11 @@
show "finite ?F"
using \<open>finite simplices\<close> unfolding F_eq by auto
- { fix f assume "f \<in> ?F" "bnd f" then show "card {s \<in> simplices. face f s} = 1"
- using bnd by auto }
+ show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
+ using bnd prems by auto
- { fix f assume "f \<in> ?F" "\<not> bnd f" then show "card {s \<in> simplices. face f s} = 2"
- using nbnd by auto }
+ show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
+ using nbnd prems by auto
show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
using odd_card by simp