Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
authorwenzelm
Tue, 09 Oct 2012 22:24:24 +0200
changeset 49751 5248806bc7ab
parent 49750 444cfaa331c9
child 49752 2bbb0013ff82
removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;
src/HOL/Library/Univ_Poly.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Univ_Poly.thy	Tue Oct 09 21:33:12 2012 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Tue Oct 09 22:24:24 2012 +0200
@@ -414,7 +414,6 @@
 apply (auto simp add: poly_exp poly_mult)
 done
 
-lemma (in semiring_1) one_neq_zero[simp]: "1 \<noteq> 0" using zero_neq_one by blast
 lemma (in comm_ring_1) poly_prime_eq_zero[simp]: "poly [a,1] \<noteq> poly []"
 apply (simp add: fun_eq)
 apply (rule_tac x = "minus one a" in exI)
isabelle