explicit dummy instantiation for div
authorhaftmann
Mon Apr 07 15:37:30 2008 +0200 (2008-04-07)
changeset 26563420567ad8125
parent 26562 9d25ef112cf6
child 26564 631ce7f6bdc6
explicit dummy instantiation for div
src/HOL/Algebra/poly/UnivPoly2.thy
     1.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 07 15:37:27 2008 +0200
     1.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 07 15:37:30 2008 +0200
     1.3 @@ -140,9 +140,19 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instance up :: (type) Divides.div ..
     1.8 +instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") Divides.div
     1.9 +begin
    1.10 +
    1.11 +definition "a div (b \<Colon> 'a up) = undefined a b"
    1.12 +
    1.13 +definition "a mod (b \<Colon> 'a up) = a - (a div b) * b"
    1.14  
    1.15 -instantiation up :: ("{times, one, comm_monoid_add}") inverse
    1.16 +instance ..
    1.17 +
    1.18 +end
    1.19 +
    1.20 +
    1.21 +instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
    1.22  begin
    1.23  
    1.24  definition