equal
deleted
inserted
replaced
3 $Id$ |
3 $Id$ |
4 Author: Clemens Ballarin, started 9 December 1996 |
4 Author: Clemens Ballarin, started 9 December 1996 |
5 *) |
5 *) |
6 |
6 |
7 Blast.overloaded ("Divides.op dvd", domain_type); |
7 Blast.overloaded ("Divides.op dvd", domain_type); |
|
8 |
|
9 val a_assoc = thm "plus_ac0.assoc"; |
|
10 val l_zero = thm "plus_ac0.zero"; |
|
11 val a_comm = thm "plus_ac0.commute"; |
8 |
12 |
9 section "Rings"; |
13 section "Rings"; |
10 |
14 |
11 fun make_left_commute assoc commute s = |
15 fun make_left_commute assoc commute s = |
12 [rtac (commute RS trans) 1, rtac (assoc RS trans) 1, |
16 [rtac (commute RS trans) 1, rtac (assoc RS trans) 1, |