src/HOL/Power.thy

--- a/src/HOL/Power.thy	Thu May 14 15:09:47 2009 +0200
+++ b/src/HOL/Power.thy	Thu May 14 15:09:47 2009 +0200
@@ -452,4 +452,13 @@
   from power_strict_increasing_iff [OF this] less show ?thesis ..
 qed
 
+
+subsection {* Code generator tweak *}
+
+lemma power_power_power [code, code unfold, code inline del]:
+  "power = power.power (1::'a::{power}) (op *)"
+  unfolding power_def power.power_def ..
+
+declare power.power.simps [code]
+
 end