# HG changeset patch
# User berghofe
# Date 1170865853 -3600
# Node ID 6a65e9b2ae056f67e9e1286464a9dd6a0fa88e21
# Parent  990a638e6f69d3dacf4d884fa18f9d60f1f38986
Theorems for converting between wf and wfP are now declared
as hints.

diff -r 990a638e6f69 -r 6a65e9b2ae05 src/HOL/Recdef.thy
--- 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 . . . *)