--- a/src/HOL/Integ/NatBin.thy Thu Sep 29 15:50:46 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy Thu Sep 29 17:02:57 2005 +0200
@@ -268,10 +268,10 @@
lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
by (simp add: numeral_2_eq_2 Power.power_Suc)
-lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
+lemma zero_power2 [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
by (simp add: power2_eq_square)
-lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
+lemma one_power2 [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
by (simp add: power2_eq_square)
lemma power3_eq_cube: "(x::'a::recpower) ^ 3 = x * x * x"