src/HOL/Integ/NatBin.thy
changeset 17085 5b57f995a179
parent 16775 c1b87ef4a1c3
child 17550 9bcd6ea262b8
--- 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]
+