# HG changeset patch # User berghofe # Date 1184144955 -7200 # Node ID d6349ac8b153a06c28b74415fd92cc98aa41abcb # Parent 1801a921df13ceaa25edb80d3315d8a6af7094a8 Removed wf_implies_wfP and wfP_implies_wf from list of hints again. diff -r 1801a921df13 -r d6349ac8b153 src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Wed Jul 11 11:07:57 2007 +0200 +++ b/src/HOL/Recdef.thy Wed Jul 11 11:09:15 2007 +0200 @@ -75,7 +75,5 @@ wf_pred_nat wf_same_fst wf_empty - wf_implies_wfP - wfP_implies_wf end