| changeset 45231 | d85a2fdc586c |
| parent 41550 | efa734d9b221 |
| child 47191 | ebd8c46d156b |
--- a/src/HOL/Power.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Power.thy Fri Oct 21 11:17:14 2011 +0200 @@ -460,7 +460,7 @@ subsection {* Code generator tweak *} -lemma power_power_power [code, code_unfold, code_inline del]: +lemma power_power_power [code]: "power = power.power (1::'a::{power}) (op *)" unfolding power_def power.power_def ..