src/HOL/Recdef.thy
changeset 23742 d6349ac8b153
parent 23150 073a65f0bc40
child 26748 4d51ddd6aa5c
--- 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