ring includes plus_ac0;
authorwenzelm
Mon Oct 15 20:34:12 2001 +0200 (2001-10-15)
changeset 1177837efbe093d3c
parent 11777 b03c8a3fcc6d
child 11779 1aa328cb273a
ring includes plus_ac0;
src/HOL/Algebra/abstract/Ring.ML
src/HOL/Algebra/abstract/Ring.thy
     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.5  Blast.overloaded ("Divides.op dvd", domain_type);
     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"