diff -r a70934b63910 -r aa158e145ea3 src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Wed Jun 06 17:00:09 2007 +0200 +++ b/src/HOL/NatBin.thy Wed Jun 06 17:01:33 2007 +0200 @@ -274,13 +274,13 @@ We cannot prove general results about the numeral @{term "-1"}, so we have to use @{term "- 1"} instead.*} -lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\ = a * a" +lemma power2_eq_square: "(a::'a::recpower)\ = a * a" by (simp add: numeral_2_eq_2 Power.power_Suc) -lemma zero_power2 [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\ = 0" +lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\ = 0" by (simp add: power2_eq_square) -lemma one_power2 [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\ = 1" +lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\ = 1" by (simp add: power2_eq_square) lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"