1.1 --- a/src/HOL/Recdef.thy	Wed Feb 07 17:29:41 2007 +0100
     1.2 +++ b/src/HOL/Recdef.thy	Wed Feb 07 17:30:53 2007 +0100
     1.3 @@ -79,6 +79,8 @@
     1.4    wf_pred_nat
     1.5    wf_same_fst
     1.6    wf_empty
     1.7 +  wf_implies_wfP
     1.8 +  wfP_implies_wf
     1.9  
    1.10  (* The following should really go into Datatype or Finite_Set, but
    1.11  each one lacks the other theory as a parent . . . *)