
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})\<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"




