src/HOL/Number_Theory/Gauss.thy
changeset 56544 b60d5d119489
parent 55730 97ff9276e12d
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4    by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
     1.5  
     1.6  lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
     1.7 -  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
     1.8 +  using a_nonzero by (auto simp add: B_def A_greater_zero)
     1.9  
    1.10  lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
    1.11  proof (auto simp add: C_def)