author | haftmann |
Thu, 06 Aug 2015 19:12:09 +0200 | |
changeset 60866 | 7f562aa4eb4b |
parent 60865 | 4194901fd513 |
child 60867 | 86e7560e07d0 |
src/HOL/Power.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Power.thy Fri Aug 07 17:58:12 2015 +0200 +++ b/src/HOL/Power.thy Thu Aug 06 19:12:09 2015 +0200 @@ -912,12 +912,6 @@ subsection \<open>Code generator tweak\<close> -lemma power_power_power [code]: - "power = power.power (1::'a::{power}) (op *)" - unfolding power_def power.power_def .. - -declare power.power.simps [code] - code_identifier code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith