src/HOL/Code_Eval.thy
changeset 31998 2c7a24f74db9
parent 31746 75fe3304015c
child 32069 6d28bbd33e2c
     1.1 --- a/src/HOL/Code_Eval.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
     1.5    "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
     1.6  
     1.7 -lemma valapp_code [code, code inline]:
     1.8 +lemma valapp_code [code, code_inline]:
     1.9    "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
    1.10    by (simp only: valapp_def fst_conv snd_conv)
    1.11