changeset 50766 | 5248806bc7ab |
parent 47604 | e3b99d0231bc |
child 50977 | a8cc904a6820 |
1.1 --- a/src/HOL/Library/Univ_Poly.thy Tue Oct 09 21:33:12 2012 +0200 1.2 +++ b/src/HOL/Library/Univ_Poly.thy Tue Oct 09 22:24:24 2012 +0200 1.3 @@ -414,7 +414,6 @@ 1.4 apply (auto simp add: poly_exp poly_mult) 1.5 done 1.6 1.7 -lemma (in semiring_1) one_neq_zero[simp]: "1 \<noteq> 0" using zero_neq_one by blast 1.8 lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \<noteq> poly []" 1.9 apply (simp add: fun_eq) 1.10 apply (rule_tac x = "minus one a" in exI)