| changeset 37767 | a2b7a20d6ea3 |
| parent 35416 | d8d7d1b785af |
| child 38554 | f8999e19dd49 |
--- a/src/HOL/Recdef.thy Mon Jul 12 08:58:27 2010 +0200 +++ b/src/HOL/Recdef.thy Mon Jul 12 10:48:37 2010 +0200 @@ -38,7 +38,7 @@ definition wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where - [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" + "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" subsection{*Well-Founded Recursion*}