1.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Sep 04 11:53:39 2014 +0200
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Sep 04 14:02:37 2014 +0200
     1.3 @@ -20,6 +20,9 @@
     1.4  apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
     1.5  done
     1.6  
     1.7 +lemma tfl_cut_def: "cut f r x \<equiv> (\<lambda>y. if (y,x) \<in> r then f y else undefined)"
     1.8 +  unfolding cut_def .
     1.9 +
    1.10  lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
    1.11  apply clarify
    1.12  apply (rule cut_apply, assumption)