src/HOL/Divides.thy
changeset 14430 5cb24165a2e1
parent 14267 b963e9cee2a0
child 14437 92f6aa05b7bb
     1.1 --- a/src/HOL/Divides.thy	Thu Mar 04 10:06:13 2004 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Mar 04 12:06:07 2004 +0100
     1.3 @@ -14,8 +14,6 @@
     1.4    div < type
     1.5  
     1.6  instance  nat :: div ..
     1.7 -instance  nat :: plus_ac0
     1.8 -proof qed (rule add_commute add_assoc add_0)+
     1.9  
    1.10  consts
    1.11    div  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)