| changeset 22737 | d87ccbcc2702 |
| parent 21414 | 4cb808163adc |
| child 24304 | 69d40a562ba4 |
--- a/src/HOL/Relation_Power.thy Fri Apr 20 11:21:34 2007 +0200 +++ b/src/HOL/Relation_Power.thy Fri Apr 20 11:21:35 2007 +0200 @@ -40,7 +40,8 @@ *} definition - funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where + funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" +where funpow_def: "funpow n f = f ^ n" lemmas [code inline] = funpow_def [symmetric]