src/HOL/Recdef.thy
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 . . . *)