# HG changeset patch
# User haftmann
# Date 1242306587 -7200
# Node ID 92d8ff6af82c9b975042ee871ff3cd7a8827a2c4
# Parent  f919b8e67413d5dc9060e17830c00f1285b99f0b
monomorphic code generation for power operations

diff -r f919b8e67413 -r 92d8ff6af82c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu May 14 15:09:47 2009 +0200
+++ b/src/HOL/Nat.thy	Thu May 14 15:09:47 2009 +0200
@@ -1199,7 +1199,7 @@
 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   funpow_code_def [code post]: "funpow = compow"
 
-lemmas [code inline] = funpow_code_def [symmetric]
+lemmas [code unfold] = funpow_code_def [symmetric]
 
 lemma [code]:
   "funpow 0 f = id"
diff -r f919b8e67413 -r 92d8ff6af82c 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