| changeset 39198 | f967a16dfcdd |
| parent 38554 | f8999e19dd49 |
| child 39302 | d7728f65b353 |
--- a/src/HOL/Recdef.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Recdef.thy Tue Sep 07 10:05:19 2010 +0200 @@ -45,7 +45,7 @@ text{*cut*} lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" -by (simp add: expand_fun_eq cut_def) +by (simp add: ext_iff cut_def) lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" by (simp add: cut_def)