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 (* |
7 (* |
8 val a_assoc = thm "plus_ac0.assoc"; |
8 val a_assoc = thm "semigroup_add.add_assoc"; |
9 val l_zero = thm "plus_ac0.zero"; |
9 val l_zero = thm "comm_monoid_add.add_0"; |
10 val a_comm = thm "plus_ac0.commute"; |
10 val a_comm = thm "ab_semigroup_add.add_commute"; |
11 |
11 |
12 section "Rings"; |
12 section "Rings"; |
13 |
13 |
14 fun make_left_commute assoc commute s = |
14 fun make_left_commute assoc commute s = |
15 [rtac (commute RS trans) 1, rtac (assoc RS trans) 1, |
15 [rtac (commute RS trans) 1, rtac (assoc RS trans) 1, |