| changeset 31021 | 53642251a04f |
| parent 30968 | 10fef94f40fc |
| child 35028 | 108662d50512 |
--- a/src/HOL/NSA/StarDef.thy Tue Apr 28 19:15:50 2009 +0200 +++ b/src/HOL/NSA/StarDef.thy Wed Apr 29 14:20:26 2009 +0200 @@ -954,8 +954,6 @@ subsection {* Power *} -instance star :: (recpower) recpower .. - lemma star_power_def [transfer_unfold]: "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x" proof (rule eq_reflection, rule ext, rule ext)