author | haftmann |
Tue, 07 Oct 2008 16:07:22 +0200 | |
changeset 28517 | dd46786d4f95 |
parent 28516 | e6fdcaaadbd3 |
child 28518 | 0329689a1127 |
--- a/src/HOL/Relation_Power.thy Tue Oct 07 16:07:21 2008 +0200 +++ b/src/HOL/Relation_Power.thy Tue Oct 07 16:07:22 2008 +0200 @@ -54,7 +54,7 @@ "fun_pow 0 f = id" | "fun_pow (Suc n) f = f o fun_pow n f" -lemma funpow_fun_pow [code inline]: "f ^ n = fun_pow n f" +lemma funpow_fun_pow [code unfold]: "f ^ n = fun_pow n f" unfolding funpow_def fun_pow_def .. lemma funpow_add: "f ^ (m+n) = f^m o f^n"