equal
deleted
inserted
replaced
38 text {* |
38 text {* |
39 Circumvent this problem for code generation: |
39 Circumvent this problem for code generation: |
40 *} |
40 *} |
41 |
41 |
42 definition |
42 definition |
43 funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where |
43 funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
|
44 where |
44 funpow_def: "funpow n f = f ^ n" |
45 funpow_def: "funpow n f = f ^ n" |
45 |
46 |
46 lemmas [code inline] = funpow_def [symmetric] |
47 lemmas [code inline] = funpow_def [symmetric] |
47 |
48 |
48 lemma [code func]: |
49 lemma [code func]: |