src/HOL/Divides.thy
changeset 8961 b547482dd127
parent 8902 a705822f4e2a
child 10212 33fe2d701ddd
     1.1 --- a/src/HOL/Divides.thy	Wed May 24 18:48:03 2000 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed May 24 18:48:22 2000 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4  axclass
     1.5    div < term
     1.6  
     1.7 -instance
     1.8 -  nat :: div
     1.9 +instance  nat :: div
    1.10 +instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)
    1.11  
    1.12  consts
    1.13    div  :: ['a::div, 'a]  => 'a          (infixl 70)