installing plus_ac0 for nat
authorpaulson
Wed May 24 18:48:22 2000 +0200 (2000-05-24)
changeset 8961b547482dd127
parent 8960 0cd01ec1830b
child 8962 633e1682455c
installing plus_ac0 for nat
src/HOL/Divides.thy
     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)