src/HOL/Power.thy
changeset 31155 92d8ff6af82c
parent 31021 53642251a04f
child 31998 2c7a24f74db9
     1.1 --- a/src/HOL/Power.thy	Thu May 14 15:09:47 2009 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu May 14 15:09:47 2009 +0200
     1.3 @@ -452,4 +452,13 @@
     1.4    from power_strict_increasing_iff [OF this] less show ?thesis ..
     1.5  qed
     1.6  
     1.7 +
     1.8 +subsection {* Code generator tweak *}
     1.9 +
    1.10 +lemma power_power_power [code, code unfold, code inline del]:
    1.11 +  "power = power.power (1::'a::{power}) (op *)"
    1.12 +  unfolding power_def power.power_def ..
    1.13 +
    1.14 +declare power.power.simps [code]
    1.15 +
    1.16  end