author wenzelm Mon Oct 15 20:34:12 2001 +0200 (2001-10-15) changeset 11778 37efbe093d3c parent 11777 b03c8a3fcc6d child 11779 1aa328cb273a
ring includes plus_ac0;
```     1.1 --- a/src/HOL/Algebra/abstract/Ring.ML	Mon Oct 15 20:33:42 2001 +0200
1.2 +++ b/src/HOL/Algebra/abstract/Ring.ML	Mon Oct 15 20:34:12 2001 +0200
1.3 @@ -6,6 +6,10 @@
1.4
1.6
1.7 +val a_assoc = thm "plus_ac0.assoc";
1.8 +val l_zero = thm "plus_ac0.zero";
1.9 +val a_comm = thm "plus_ac0.commute";
1.10 +
1.11  section "Rings";
1.12
1.13  fun make_left_commute assoc commute s =
```
```     2.1 --- a/src/HOL/Algebra/abstract/Ring.thy	Mon Oct 15 20:33:42 2001 +0200
2.2 +++ b/src/HOL/Algebra/abstract/Ring.thy	Mon Oct 15 20:34:12 2001 +0200
2.3 @@ -27,12 +27,12 @@
2.4  (* Class ring and ring axioms *)
2.5
2.6  axclass
2.7 -  ring < ringS
2.8 +  ring < ringS, plus_ac0
2.9
2.10 -  a_assoc	"(a + b) + c = a + (b + c)"
2.11 -  l_zero	"0 + a = a"
2.12 +(*a_assoc	"(a + b) + c = a + (b + c)"*)
2.13 +(*l_zero	"0 + a = a"*)
2.14    l_neg		"(-a) + a = 0"
2.15 -  a_comm	"a + b = b + a"
2.16 +(*a_comm	"a + b = b + a"*)
2.17
2.18    m_assoc	"(a * b) * c = a * (b * c)"
2.19    l_one		"<1> * a = a"
```