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