src/HOL/Parity.thy
changeset 61531 ab2e862263e7
parent 60867 86e7560e07d0
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 29 15:40:52 2015 +0100
     1.2 +++ b/src/HOL/Parity.thy	Mon Nov 02 11:56:28 2015 +0100
     1.3 @@ -233,7 +233,7 @@
     1.4  
     1.5  subsection \<open>Parity and powers\<close>
     1.6  
     1.7 -context comm_ring_1
     1.8 +context ring_1
     1.9  begin
    1.10  
    1.11  lemma power_minus_even [simp]: