| changeset 3320 | 3a5e4930fb77 |
| parent 3198 | 295287618e30 |
| child 3413 | c1f63cc3a768 |
--- a/src/HOL/WF.ML Fri May 23 14:52:45 1997 +0200 +++ b/src/HOL/WF.ML Fri May 23 18:17:53 1997 +0200 @@ -102,7 +102,7 @@ (*** is_recfun ***) goalw WF.thy [is_recfun_def,cut_def] - "!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = (@z.True)"; + "!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = arbitrary"; by (etac ssubst 1); by (asm_simp_tac HOL_ss 1); qed "is_recfun_undef";