| changeset 56544 | b60d5d119489 |
| parent 49962 | a8cc904a6820 |
| child 57418 | 6ab1c7cb0b8d |
--- a/src/HOL/Old_Number_Theory/Gauss.thy Fri Apr 11 23:22:00 2014 +0200 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Sat Apr 12 17:26:27 2014 +0200 @@ -175,7 +175,7 @@ done lemma B_greater_zero: "x \<in> B ==> 0 < x" - using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero) + using a_nonzero by (auto simp add: B_def A_greater_zero) lemma C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)" apply (auto simp add: C_def)