src/HOL/Power.thy
changeset 60866 7f562aa4eb4b
parent 60758 d8d85a8172b5
child 60867 86e7560e07d0
--- 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