src/HOL/Relation_Power.thy
changeset 28517 dd46786d4f95
parent 26799 5bd38256ce5b
child 29654 24e73987bfe2
     1.1 --- a/src/HOL/Relation_Power.thy	Tue Oct 07 16:07:21 2008 +0200
     1.2 +++ b/src/HOL/Relation_Power.thy	Tue Oct 07 16:07:22 2008 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    "fun_pow 0 f = id"
     1.5    | "fun_pow (Suc n) f = f o fun_pow n f"
     1.6  
     1.7 -lemma funpow_fun_pow [code inline]: "f ^ n = fun_pow n f"
     1.8 +lemma funpow_fun_pow [code unfold]: "f ^ n = fun_pow n f"
     1.9    unfolding funpow_def fun_pow_def ..
    1.10  
    1.11  lemma funpow_add: "f ^ (m+n) = f^m o f^n"