src/HOL/Power.thy
changeset 60866 7f562aa4eb4b
parent 60758 d8d85a8172b5
child 60867 86e7560e07d0
     1.1 --- a/src/HOL/Power.thy	Fri Aug 07 17:58:12 2015 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Aug 06 19:12:09 2015 +0200
     1.3 @@ -912,12 +912,6 @@
     1.4  
     1.5  subsection \<open>Code generator tweak\<close>
     1.6  
     1.7 -lemma power_power_power [code]:
     1.8 -  "power = power.power (1::'a::{power}) (op *)"
     1.9 -  unfolding power_def power.power_def ..
    1.10 -
    1.11 -declare power.power.simps [code]
    1.12 -
    1.13  code_identifier
    1.14    code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    1.15