equal
deleted
inserted
replaced
1 (* |
1 (* |
2 Abstract class ring (commutative, with 1) |
2 Abstract class ring (commutative, with 1) |
3 $Id$ |
3 $Id$ |
4 Author: Clemens Ballarin, started 9 December 1996 |
4 Author: Clemens Ballarin, started 9 December 1996 |
5 *) |
5 *) |
6 |
|
7 Blast.overloaded ("Divides.op dvd", domain_type); |
|
8 |
6 |
9 val a_assoc = thm "plus_ac0.assoc"; |
7 val a_assoc = thm "plus_ac0.assoc"; |
10 val l_zero = thm "plus_ac0.zero"; |
8 val l_zero = thm "plus_ac0.zero"; |
11 val a_comm = thm "plus_ac0.commute"; |
9 val a_comm = thm "plus_ac0.commute"; |
12 |
10 |