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