src/HOL/Library/Polynomial.thy
changeset 45605 a89b4bc311a5
parent 44890 22f665a2e91c
child 45694 4a8743618257
     1.1 --- a/src/HOL/Library/Polynomial.thy	Sun Nov 20 20:59:30 2011 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Nov 20 21:05:23 2011 +0100
     1.3 @@ -928,11 +928,9 @@
     1.4  lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
     1.5  by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
     1.6  
     1.7 -lemmas pdivmod_rel_unique_div =
     1.8 -  pdivmod_rel_unique [THEN conjunct1, standard]
     1.9 +lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
    1.10  
    1.11 -lemmas pdivmod_rel_unique_mod =
    1.12 -  pdivmod_rel_unique [THEN conjunct2, standard]
    1.13 +lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
    1.14  
    1.15  instantiation poly :: (field) ring_div
    1.16  begin