--- a/src/HOL/Parity.thy Thu Oct 29 15:40:52 2015 +0100 +++ b/src/HOL/Parity.thy Mon Nov 02 11:56:28 2015 +0100 @@ -233,7 +233,7 @@ subsection \<open>Parity and powers\<close> -context comm_ring_1 +context ring_1 begin lemma power_minus_even [simp]: