obsolete since no code generator without dictionary construction left
authorhaftmann
Thu, 06 Aug 2015 19:12:09 +0200
changeset 60866 7f562aa4eb4b
parent 60865 4194901fd513
child 60867 86e7560e07d0
obsolete since no code generator without dictionary construction left
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