Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Polynomial.thy
changeset 64592 7759f1766189
parent 64591 240a39af9ec4
child 64635 255741c5f862 
--- a/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:14 2016 +0100
@@ -2274,12 +2274,6 @@
   from pdivmod_rel[of x y,unfolded pdivmod_rel_def]
   show "x div y * y + x mod y = x" by auto
 next
-  fix x :: "'a poly"
-  show "x div 0 = 0" by simp
-next
-  fix y :: "'a poly"
-  show "0 div y = 0" by simp
-next
   fix x y z :: "'a poly"
   assume "y \<noteq> 0"
   hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
isabelle