--- 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})\<twosuperior> = a * a"
+lemma power2_eq_square: "(a::'a::recpower)\<twosuperior> = a * a"
by (simp add: numeral_2_eq_2 Power.power_Suc)
-lemma zero_power2 [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
+lemma zero_power2 [simp]: "(0::'a::{semiring_1,recpower})\<twosuperior> = 0"
by (simp add: power2_eq_square)
-lemma one_power2 [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
+lemma one_power2 [simp]: "(1::'a::{semiring_1,recpower})\<twosuperior> = 1"
by (simp add: power2_eq_square)
lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"