# HG changeset patch
# User haftmann
# Date 1438881129 -7200
# Node ID 7f562aa4eb4be91577e0cb13d98c8625b738f110
# Parent  4194901fd513d82252e268febe4e1fa249e9f1d3
obsolete since no code generator without dictionary construction left

diff -r 4194901fd513 -r 7f562aa4eb4b src/HOL/Power.thy
--- 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