| changeset 22264 | 6a65e9b2ae05 |
| parent 19770 | be5c23ebe1eb |
| child 22399 | 80395c2c40cc |
--- a/src/HOL/Recdef.thy Wed Feb 07 17:29:41 2007 +0100 +++ b/src/HOL/Recdef.thy Wed Feb 07 17:30:53 2007 +0100 @@ -79,6 +79,8 @@ wf_pred_nat wf_same_fst wf_empty + wf_implies_wfP + wfP_implies_wf (* The following should really go into Datatype or Finite_Set, but each one lacks the other theory as a parent . . . *)