--- a/src/HOL/Nat_Numeral.thy Wed Apr 22 19:09:19 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Wed Apr 22 19:09:21 2009 +0200
@@ -28,9 +28,12 @@
"nat (number_of v) = number_of v"
unfolding nat_number_of_def ..
+context recpower
+begin
+
abbreviation (xsymbols)
- power2 :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
- "x\<twosuperior> == x^2"
+ power2 :: "'a \<Rightarrow> 'a" ("(_\<twosuperior>)" [1000] 999) where
+ "x\<twosuperior> \<equiv> x ^ 2"
notation (latex output)
power2 ("(_\<twosuperior>)" [1000] 999)
@@ -38,6 +41,8 @@
notation (HTML output)
power2 ("(_\<twosuperior>)" [1000] 999)
+end
+
subsection {* Predicate for negative binary numbers *}
@@ -397,8 +402,8 @@
by (simp add: power_even_eq)
lemma power_minus_even [simp]:
- "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
-by (simp add: power_minus1_even power_minus [of a])
+ "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
+ by (simp add: power_minus [of a])
lemma zero_le_even_power'[simp]:
"0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
@@ -972,4 +977,4 @@
Suc_mod_eq_add3_mod [of _ "number_of v", standard]
declare Suc_mod_eq_add3_mod_number_of [simp]
-end
+end
\ No newline at end of file