--- a/src/HOL/Integ/NatBin.thy Tue Aug 16 15:36:28 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy Tue Aug 16 18:53:11 2005 +0200
@@ -284,7 +284,10 @@
done
text{*Squares of literal numerals will be evaluated.*}
-declare power2_eq_square [of "number_of w", standard, simp]
+lemmas power2_eq_square_number_of =
+ power2_eq_square [of "number_of w", standard]
+declare power2_eq_square_number_of [simp]
+
lemma zero_le_power2: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
by (simp add: power2_eq_square zero_le_square)
@@ -543,7 +546,9 @@
split add: split_if cong: imp_cong)
-declare power_nat_number_of [of _ "number_of w", standard, simp]
+lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
+declare power_nat_number_of_number_of [simp]
+
text{*For the integers*}
@@ -569,8 +574,14 @@
apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
done
-declare zpower_number_of_even [of "number_of v", standard, simp]
-declare zpower_number_of_odd [of "number_of v", standard, simp]
+lemmas zpower_number_of_even_number_of =
+ zpower_number_of_even [of "number_of v", standard]
+declare zpower_number_of_even_number_of [simp]
+
+lemmas zpower_number_of_odd_number_of =
+ zpower_number_of_odd [of "number_of v", standard]
+declare zpower_number_of_odd_number_of [simp]
+