changeset 12338 | de0f4a63baa5 |
parent 10789 | 260fa2c67e3e |
child 13152 | 2a54f99b44b3 |
--- a/src/HOL/Divides.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/Divides.thy Sat Dec 01 18:52:32 2001 +0100 @@ -11,7 +11,7 @@ (*We use the same class for div and mod; moreover, dvd is defined whenever multiplication is*) axclass - div < term + div < type instance nat :: div instance nat :: plus_ac0 (add_commute,add_assoc,add_0)