src/HOL/Algebra/abstract/Ring2.thy
changeset 39159 0dec18004e75
parent 38715 6513ea67d95d
child 42768 4db4a8b164c1
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -211,11 +211,11 @@
     1.4  fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
     1.5  
     1.6  val ring_ss = HOL_basic_ss settermless termless_ring addsimps
     1.7 -  [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
     1.8 -   thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def",
     1.9 -   thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add",
    1.10 -   thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*)
    1.11 -   thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"];
    1.12 +  [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
    1.13 +   @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
    1.14 +   @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},
    1.15 +   @{thm minus_minus}, @{thm minus0}, @{thm a_lcomm}, @{thm m_lcomm}, (*@{thm r_one},*)
    1.16 +   @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
    1.17  *}   (* Note: r_one is not necessary in ring_ss *)
    1.18  
    1.19  method_setup ring =