--- a/src/HOL/Algebra/Sylow.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Algebra/Sylow.thy Sun Oct 21 14:53:44 2007 +0200
@@ -126,7 +126,7 @@
apply (blast intro: one_closed zero_less_card_empty)
done
-lemma (in sylow) zero_less_m: "0 < m"
+lemma (in sylow) zero_less_m: "m \<noteq> 0"
apply (cut_tac zero_less_o_G)
apply (simp add: order_G)
done
@@ -134,7 +134,7 @@
lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a"
by (simp add: calM_def n_subsets order_G [symmetric] order_def)
-lemma (in sylow) zero_less_card_calM: "0 < card calM"
+lemma (in sylow) zero_less_card_calM: "card calM \<noteq> 0"
by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
lemma (in sylow) max_p_div_calM: