| changeset 14353 | 79f9fbef9106 |
| parent 14271 | 8ed6989228bb |
| child 14981 | e73f8140af78 |
--- a/src/HOL/NumberTheory/Gauss.thy Mon Jan 12 16:45:35 2004 +0100 +++ b/src/HOL/NumberTheory/Gauss.thy Mon Jan 12 16:51:45 2004 +0100 @@ -180,7 +180,7 @@ lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x"; apply (insert a_nonzero) -by (auto simp add: B_def zmult_pos A_greater_zero) +by (auto simp add: B_def mult_pos A_greater_zero) lemma (in GAUSS) C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)"; apply (auto simp add: C_def)